Thomas Sewell
083a4b68d7
Really add binary verification to regression test.
2014-09-08 16:23:10 +10:00
Thomas Sewell
41c0e994ad
Make SIMPL->Graph regression testable.
2014-09-05 19:10:03 +10:00
Andrew Boyton
7693e1fadc
TakeGrant: Rename a couple of constants to make things clearer.
...
has_at_least => cap_in_caps
has_at_most => caps_dominated_by
2014-09-04 14:13:46 +10:00
Thomas Sewell
4c7ef803d7
SEL4GraphRefine now completed.
...
These final changes complete the SEL4GraphRefine process. Some
cleanup remains to be done, especially in SEL4GlobalsSwap, but the
process is now mature and working, and the testing code
in SEL4GraphRefine can be discarded.
Success depends on seL4 commit 97d6bc96d54f1f0beafb25033b03b57ba54a5113
which is compatible with crefine and will be included in the repo
manifest immediately.
2014-09-03 17:38:45 +10:00
Joel Beeren
a5f2cab271
Merge branch 'master' into ioapic
2014-09-02 11:13:55 +10:00
Joel Beeren
8fa6226ecc
ioapic: fixed specs for change to 14 bit FSR
2014-09-01 16:41:33 +10:00
Thomas Sewell
caf0529c7f
Move burden of 'halt' proof, use less modifies.
...
In detail:
- add a general user-specified exception to c_exntype
(for use in tools like Substitute)
- wrap calls to 'halt' in Guard {}, making it clearer that
halt is never called, simplifying asmrefine
- repair halt changes in crefine
- avoid use of some suspicious 'modifies' properties in crefine
which were generated by the parser for functions where inline
ASM blocks have been elided, and which may be inaccurate.
2014-08-29 13:57:28 +10:00
Joel Beeren
463df8e083
Merge branch 'master' into ioapic
2014-08-29 13:14:53 +10:00
Joel Beeren
b3e2eb1f9d
ioapic: finished up to InfoFlowC
2014-08-28 15:56:26 +10:00
Thomas Sewell
0346fb20b6
SIMPL->Graph proofs largely working.
2014-08-27 15:30:34 +10:00
Joel Beeren
8d11a22f5b
ioapic: first abstract spec
2014-08-22 16:24:40 +10:00
Thomas Sewell
0c52978dd8
More asmrefine work, global swapping ready.
2014-08-21 14:13:46 +10:00
Gerwin Klein
f1d808c96a
integrate separation kernel config proofs
...
Hooked up into build system and regression test; added READMEs
2014-08-13 22:08:46 +10:00
Gerwin Klein
3556bee2dc
github import of static cap config proofs
2014-08-13 15:31:21 +10:00
David Greenaway
5ab730970b
autocorres: Remove unnecessary rule from "whileLoop_results".
...
Thanks Tom for spotting this while proofing my thesis.
2014-08-13 12:18:46 +10:00
Gerwin Klein
7b20cbdf9d
add DOI
2014-08-11 15:50:09 +10:00
Gerwin Klein
246ef58819
Proof contributors
2014-08-08 14:28:57 +10:00
Gerwin Klein
56c93597e3
further README tweak
2014-08-03 13:11:09 +10:00
Gerwin Klein
424463426d
More dependency description; added Mac cpp wrapper
...
Based on suggestions by @jserv and @bacam
See also https://github.com/seL4/l4v/pull/1
2014-08-03 13:01:58 +10:00
Gerwin Klein
dbcc450e31
add full latex dependencies
2014-07-28 22:09:37 +02:00
Gerwin Klein
9adbb9873d
add Isabelle dependencies
2014-07-28 21:27:46 +02:00
Gerwin Klein
8958f02c34
64bit by default, so C proofs work.
2014-07-28 17:49:17 +02:00
Gerwin Klein
4565c7bf14
tune build instructions
2014-07-28 17:49:07 +02:00
Gerwin Klein
4a62bf5bfd
ignore generated files
2014-07-28 11:35:31 +02:00
Gerwin Klein
ef7ba847c0
bump API version
2014-07-28 11:10:47 +02:00
Corey Lewis
71ad3eed07
Update a comment in the capDL spec.
2014-07-28 17:45:50 +10:00
David Greenaway
0fb7a8084d
misc: Proofing and formatting of README.md files.
...
Attempt to improve readability of the files when viewed as plain ASCII;
proof-read and fix minor issues.
2014-07-28 13:15:48 +10:00
Matthew Fernandez
c9e3233b3e
autocorres: Fix WordLib import.
2014-07-27 17:14:22 -07:00
Gerwin Klein
f126d8bf45
adjust isabelle paths for standalone `make`
2014-07-27 20:25:04 +02:00
Gerwin Klein
cd6abfb096
added README.md
2014-07-27 20:24:24 +02:00
Gerwin Klein
007c5e49c9
make mlton the default for standalone tools
...
polyml has too many problems with 64bit dependencies
2014-07-27 20:02:24 +02:00
Andrew Boyton
63c6ef2785
Updated READMEs for capDL-api and sep-capDL, and added one for sys-init.
2014-07-26 12:28:38 +10:00
Toby Murray
35b6099732
remaining README.md for proof/
2014-07-25 11:51:31 +10:00
David Greenaway
7623c07355
autocorres: Delete obsolete README file.
2014-07-25 11:35:13 +10:00
David Greenaway
b304df74ca
autocorres: Create basic README.md file.
2014-07-25 11:34:28 +10:00
Corey Lewis
1421b09366
Even more cleanup of drefine.
2014-07-25 11:23:24 +10:00
Andrew Boyton
c060f715db
Add a top-level file for the capDL API proofs.
2014-07-24 19:56:24 +10:00
Toby Murray
283b54b351
comment to explain different do_user_op function in infoflow ADT
2014-07-24 14:53:57 +10:00
Toby Murray
b57c8ca1e4
README.md for tools/
2014-07-24 13:58:16 +10:00
Toby Murray
93375ba96d
Initial README.md files for proof/
2014-07-24 13:31:57 +10:00
Toby Murray
30947b3e3f
add links to README.md
2014-07-24 10:49:32 +10:00
Corey Lewis
ffb0d165f6
Some more cleanup of drefine.
2014-07-23 15:29:20 +10:00
Andrew Boyton
add3ea9cd5
sys-init: Show the separation algebra for capDL is a cancellative separation algebra.
...
* The separation algebra for capDL is also a cancellative separation algebra.
* The arrows are strictly_exact, meaning they describe only a single heap.
* Since we have a cancellative separation algebra, this means the arrows are also precise.
2014-07-23 15:20:52 +10:00
Gerwin Klein
4326d30cdc
the other README files for spec/
2014-07-22 19:11:43 -04:00
Gerwin Klein
fc4200f845
README files for spec/
2014-07-22 19:10:10 -04:00
Gerwin Klein
0fa0a14f7d
filled in README
2014-07-22 18:35:05 -04:00
Gerwin Klein
154da63715
remove old levity and taint-mode comments
2014-07-22 18:10:28 +02:00
Gerwin Klein
50dda7708c
comment cleanup
2014-07-22 18:10:20 +02:00
Andrew Boyton
acf0abe16a
Cleanup of a number of definitions of the separation algebra for capDL.
...
* The definitions of the separation "arrows" is slightly nicer and more consistent.
- We have a nicer correspondence between sep_map_c and sep_map_s.
- sep_map_irq now specifies exactly what the IRQ table contains
(that it *only* has one entry, not that it contains at least that entry).
- Nicer LaTeX output for the arrows.
* A number of minor renaming of constants and types.
- cdl_component => cdl_component_id
- sep_entity => cdl_component
- state_sep_projection => sep_state_projection
- obj_to_sep_state => object_to_sep_state
* Removed a few unused lemmas.
2014-07-22 14:37:37 +10:00
Andrew Boyton
36588c4359
Minor cleanup of proofs in the Take/Grant security model.
2014-07-22 14:36:53 +10:00