adbrucker/lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
397 Commits 7 Branches 0 Tags 86 MiB
297fbebfef
Commit Graph

98 Commits

Author SHA1 Message Date
Gerwin Klein
c6564cb4cb infoflow: 2015 update for infoflow C refinement 2015-05-20 21:10:59 +10:00
Gerwin Klein
d4be402559 crefine: even more complete 2015 update 2015-05-20 21:03:48 +10:00
Gerwin Klein
bfef1e10d3 crefine: 2015 update complete 2015-05-20 20:39:47 +10:00
Gerwin Klein
eea646c84a crefine: 2015 update up to Tcb_C 2015-05-18 09:11:43 +10:00
Gerwin Klein
cba6a4f59e infoflow: minor cleanup 2015-05-16 21:49:01 +10:00
Gerwin Klein
a6f1ab41f8 ainvs: some more cleanup 2015-05-16 21:48:24 +10:00
Gerwin Klein
12fa86863a fewer warnings 2015-05-16 19:52:49 +10:00
Gerwin Klein
b46bc4e78d infoflow: 2015 update (apart from C refinement) 2015-05-16 18:14:59 +10:00
Gerwin Klein
c124554d83 Dpolicy 2015 udpate 2015-05-14 18:56:32 +02:00
Gerwin Klein
164f1db611 proof/capDL-api: 2015 update 2015-05-14 11:41:20 +02:00
Gerwin Klein
330e730fa3 retire old obsolete ADT refinement phrasing 
The observable state has been strengthened significantly years ago and
this theory has fallen into disrepair. The toplevel refinement statement
here was nicely concise for a paper, but the practical value is in the
much stronger corres statement, so instead of attempting proof
acrobatics with a new observable state, I'm retiring this theory.
 2015-05-13 10:49:30 +02:00
Gerwin Klein
f6124669fc 2015 update for DRefine 2015-05-13 09:52:32 +02:00
Gerwin Klein
0c67e0bfa1 2015 update for Refine 2015-05-12 17:17:31 +02:00
Gerwin Klein
177e5bf185 2015 update for access 2015-05-06 13:46:20 -04:00
Gerwin Klein
baa5791918 Isabelle2015 update: Bisim 2015-04-19 10:25:42 +01:00
Gerwin Klein
42e037ea9d Isabelle2015 update: AInvs 2015-04-19 10:25:21 +01:00
Gerwin Klein
f9e40c29db cleanup: there already is a separate Bisim session 2015-04-19 10:24:42 +01:00
Gerwin Klein
17826f9b49 more Isabelle2015 update; AInvs up to (excluding) Syscall_AI 
also includes some global replacements
 2015-04-18 21:51:26 +01:00
Gerwin Klein
22af66555c remove even arch calls from separation kernel setup 
(patch by Simon Winwood)
 2015-04-10 17:39:24 +10:00
Daniel Matichuk
a221a52350 Added new proofcount tool to "tools" and removed old one from "lib". 
Removed reference to old proof_counting from proof/ROOT and spec/ROOT
 2015-02-11 17:46:34 +11:00
Gerwin Klein
2e58320711 adjust for seL4 rev 28d7fda6a9128efe 2015-01-10 08:34:52 +11:00
Gerwin Klein
0466161f2d CRefine for XN 2014-11-28 08:58:57 +11:00
Gerwin Klein
29eb636d31 re-establish InfoFlow; generalising ptable_xn 
UserOp_IF had its own way of extracting the XN bit from page tables.
This is now unified with the existing functions in ADT_AI, which also
means that the proof for XN bit equality is basically the same as for
pt_rights and pt_lift.
 2014-11-28 08:58:57 +11:00
Gerwin Klein
7e7d39c24e enable XN in abstract spec; update AInvs and Refine 2014-11-28 08:58:57 +11:00
Gerwin Klein
57bef16d8e sync Makefile and test.xml 2014-11-23 19:54:59 +11:00
Gerwin Klein
118093af99 add capDL separation logic to regression test 2014-11-23 15:03:35 +11:00
Gerwin Klein
ee94da7473 de-bitrot DPolicy; add back into regression 2014-11-23 14:52:21 +11:00
deang
f9b9f9ba53 infoflow: remove s0_ptrs_distinct from Example_Valid_StateH 
subsumed by distinct command in Example_Valid_State
 2014-11-19 16:01:49 +11:00
deang
77c600038f infoflow: fixed and added Example_Valid_StateH to testing 
Some of the noninterference results depend on executions at the haskell level starting at a valid initial state. This file demonstrates this condition being realised.
 2014-11-18 17:39:17 +11:00
Gerwin Klein
dfa9c09892 abstract Haskell init parameters into constants 2014-11-06 18:48:36 +11:00
deang
f9ea932cfb noninterference: remove duplicate lemmas 
Some redundant duplicate lemmas with duplicate names were proven under locale contexts 'unwinding_system' and 'complete_unwinding_system'.
 2014-11-03 13:14:18 +11:00
David Greenaway
127c7cd63e infoflow: trivial: Add some comments to "do_user_op_if" definition. 2014-10-27 09:31:31 +11:00
David Greenaway
759a7fa8cb infoflow: trivial: Add some minor comments to "Noninterference_Base.thy". 
Added while trying to work out some details. Perhaps more useful than
not?
 2014-10-16 17:09:11 +11:00
deang
77f85b334d trivial: typo in comment 2014-10-14 17:29:47 +11:00
deang
6df2eb6cf9 infoflow: weakened assumptions for c refinement of infoflow adts 
The fact that the C infoflow adt refines the abstract infoflow adt now only requires that given user operation is nonempty and not sane (nonempty and doesn't return an interrupt).
Also added some more general lemmas about fw_sim and refinement to lib/Simulation.thy.
 2014-10-14 17:01:11 +11:00
David Greenaway
6c915fa629 infoflow: Move "EquivValid" out of "infoflow/", into "lib/". 
More importantly, remove seL4 from the dependencies of "EquivValid", so
others can use it.

Also, we fixup the fallout.
 2014-10-13 11:05:31 +11:00
David Greenaway
b0832637e6 infoflow: Change definition of "the_nat_to_bl" to avoid undefined outputs. 
...and clean up some fallout.

In particular, we now say that the output of "nat_to_bl sz n" is taken
to be the bitlist of "n mod 2^sz", so the output is always defined.

The idea is to remove the undefinedness of "the_nat_to_bl" so that it is
easier to generate simp rules for it; some of these are developed in the
theory below, and simplify some of the more concrete infoflow proofs.
 2014-10-07 08:59:17 +11:00
David Greenaway
bf2d517009 infoflow: Use the "distinct" command in "Example_Valid_State". 
Use the previously-added "distinct" command to simplify the
"Example_Valid_State" proof. This brings quite significant speedups as
it means that raw definitions need not be unfolded, and hence automated
tactics don't get side-tracked with their numerical definitions.
 2014-10-07 08:59:17 +11:00
David Greenaway
1f16bc8c2b access: Remove now-redundant "apply blast". 
Previously introduced "simp" rule makes this command redundant.
 2014-10-01 17:43:11 +10:00
Thomas Sewell
a818e13e3e Don't reuse the s_footprint_intvl theorem name. 2014-10-01 11:16:40 +10:00
Thomas Sewell
665a3c15a0 Restore global valid assertions in graph refine. 
The global-object pointer validity assertion is now created at
export time, and the graph refine mechanism now proves them. It
seems they were forgotten about once again in adjusting the globals
logic.
 2014-09-30 16:09:22 +10:00
David Greenaway
0288aeb1b8 bisim: Isabelle 2014 changes. 2014-09-24 12:24:00 +10:00
David Greenaway
df8237c08a drefine: Isabelle 2014 changes. 2014-09-24 12:21:10 +10:00
Thomas Sewell
60f06246c7 Commit some of the GraphRefine testing rig. 
Otherwise I have to fetch this out from history every
time that SEL4GraphRefine breaks.
 2014-09-23 16:40:07 +10:00
David Greenaway
0c004d2a93 Merge branch 'master' into 'isabelle-2014'. 
Conflicts:
	proof/drefine/Arch_DR.thy
	proof/drefine/Finalise_DR.thy
	proof/drefine/StateTranslation_D.thy
	sys-init/DuplicateCaps_SI.thy
	sys-init/Proof_SI.thy
	tools/autocorres/tests/examples/SchorrWaite.thy
 2014-09-23 14:31:33 +10:00
David Greenaway
22b9118432 infoflow: Fix non-terminating proof for Isabelle 2014. 
Remove useless ROOT.ML file, while I am here.
 2014-09-19 14:33:54 +10:00
Thomas Sewell
f59767cdac Slight fudges for Fastpath use with PIDE. 2014-09-18 20:12:43 +10:00
Thomas Sewell
4a56fb49f9 Fix a triviality in Interrupt_C. 2014-09-18 19:30:32 +10:00
Andrew Boyton
ea58753cd7 Merge branch 'cdl_page_map_cancel' 
Merge in the setting of registers and the starting of threads in the system initialser.
 2014-09-18 17:21:17 +10:00
Andrew Boyton
2b7b258997 sys-init: Prove the starting of threads is done correctly. 
We no longer assume the starting of threads, but prove it correct
(assuming the behaviour of the scheduler).
 2014-09-18 12:30:04 +10:00