Recent changes to the C kernel mean that various structures and
constants are generated from DTS files. In particular, verification now
sees interrupt identifiers as integer literals instead of defined
constants.
Instead of hardcoding basic C types, this passes most of them along as
uninterpreted strings. This allows typedefs such as time_t or ssize_t
to be used, without requiring the formal model to recognise them.
The proof structure still largely follows Thibaut's scheme; this commit
merely adds some speedup, style cleanup, and documentation.
Unfortunately, the proof state seems to be just large enough that the
built-in record update ruleset runs into limitations, and the standard
clasimp tactics start to fail on subgoals in an unpredictable way.
This is ostensibly more principled than the earlier proof, which simply
unfolded all the monad combinators. However, there was also no existing
framework for using monad_commute, so we need to make one up just to
do this single proof.
Mainly repercusion of changes occuring for Access:
- Fix subjectReads and subjectAffects with new authorities
- SILC label is forbidden to contain any transferable cap
- Lots of lemma that required is_subject on their parameter now only
require aag_can_read when possible
- Major cleanup of the integrity ==> subjectAffects proofs for kheap,
CDT and user memory.
Integrity and pasRefined are majorly changed
The main repercussions are:
- 3 new authorities in the policy: Call, Reply, and DeleteDerived
- The cdt and the caps state are linked in pasRefined
- CDT parentship no longer implies control in certain cases (is_transferable)
- CDT parentship now implies DeleteDerived
- Introduction of cdt_change_allowed that specifies which slot your are
allowed to modify
- Integrity for CDT and CDT list use cdt_changes_allowed
- Integrity for objects in now expressed as a transitive closure of
atomic transition rules
Uses proof body terms to disambiguate the names encoutered in
dependency extraction, rather than using (for example)
Thm.full_prop_of.
The result is that this catches a few more missing dependencies,
enough to correctly identify unused lemmas large sessions
like CRefine.
Normal abbreviations are not contracted on pretty printing when defined
inside a locale. This commit provide the command locale_abbrev which does
contract on pretty print even when defined inside a locale. It cannot be
used with abbreviations that mention fixed locale variables (whereas the
standard abbreviations can).
Co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Gerwin Klein
Matthew Brecknell
Japheth Lim
Thibaut Perami
Rafal Kolanski
Michael Sproul
Edward Pierzchalski