The rule for kernel.sigs previously depended on building standalone C
parsers and tokenizers for all architectures. With this change, we only
build the standalone C parser for the current architecture.
We also explicitly pass a --cpp argument based on the TOOLPREFIX.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
Some development environments set an environment variable OBJDUMP by
default. With the previous version of kernel.mk, decompilation used the
objdump indicated by that OBJDUMP variable. This could cause
decompilation to fail if OBJDUMP did not match the TOOLPREFIX used for
compilation.
Since we don't currently have a need to specify a different objdump, we
remove the ability to override via the OBJDUMP environment variable.
With this commit, we always use TOOLPREFIX to locate a suitable objdump.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
Add a second matrix job that runs SimplExportAndRefine for MCS C kernel
configurations that support it (currently ARM and RISCV64).
Note that this uses the master branch of l4v to generate the CSpec, and
to run SimplExportAndRefine, not the rt branch. This works because the
rt branch does not yet connect to the CSpec, and there are no meaningful
differences between rt and master in CSpec or SimplExportAndRefine. For
now, this simplifies workflows for binary verification. But when MCS
proofs connect to the CSpec, this will need to be refactored to use the
rt branch.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
Upload an artifact for any C graph-lang generated by
SimplExportAndRefine during a proof-deploy workflow.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
An invocation to bind a thread to a VCPU will perform associate_vcpu_tcb.
Previously, vcpu_switch was called only on a context switch, and so
it was possible to bind the current thread to a VCPU and then not switch
to that VCPU. This change will allow us to prove that the current active
VCPU is the VCPU of the current thread.
Signed-off-by: Michael McInerney <m.mcinerney@unsw.edu.au>
The repeat_unless method allows one to repeatedly apply some method
until some other method can be applied. This should be particularly
useful in Hoare triple proofs that use the forward-reasoning style
This commit was cherry-picked from the rt branch.
Signed-off-by: Michael McInerney <Michael.McInerney@data61.csiro.au>
These currently work with an empty prefix as well, but using the name of
the theory file containing the respective install_C_file is more stable.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Add and carry around a `pfx` parameter indicating the prefix under which
constants should be found. Without this prefix, items such as
enumeration constant names are guessed at from unqualified names. If the
unqualified name is hidden for some reason, or clobbered with another
name, the wrong constant gets used and leads to exciting errors.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Since `numDomains` exists both in Kernel_Config in C, and we want to
force people to annotate the C version as `Kernel_C.numDomains`, we hide
it right after the C is parsed.
Some of the comments about hiding/reintroducing vmsize constants became
a bit broken/absent around X64, and adding the above made things extra
confusing. Put back the ARM/ARM_HYP comments to clear up what's going
on, and tweaked a little.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This change eases any future platform ports by better matching the C
code that it models and by making it so that there is one less constant
that needs modification.
Signed-off-by: Corey Lewis <corey.lewis@unsw.edu.au>
The setup for L4V_ARCH=AARCH64 is identical to RISCV64, i.e. same word
length, encoding, and endianness. The setup includes the standalone
parser used for compile and preprocess checks in the seL4 repo.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit adds compiler prefixes for AArch64 so that the preprocess
test finds the right cross compilers for this architecture.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
${{github.ref}} will resolve to the base branch of the PR, not the
PR branch, so it is not useful for distinguishing PRs. The pull request
number will do the job.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
By default GitHub spawns a new test for each push event. To avoid
hitting the maximum number of AWS instances too quickly, we run the PR
and master proof tests only on the most recent push since the last test
finished.
The concurrency exclusion is per git ref, i.e. separate PRs and
separate branches still run tests concurrently.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This includes replacing previous ASpec names for such constants with
the names used in Haskell/ExecSpec to avoid duplication. This also
makes some of the proofs slightly more generic.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This script takes the gen_config.h file CMake produces for each kernel
configuration, parses it, and emits corresponding Isabelle definitions
into Kernel_Config.thy in spec/machine/$L4V_ARCH/
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The InfoFlow proof itself does not care about the number of domains, and
that assumption was removed in another commit.
The specific example in the information flow refinement requires two
domains (one "high" and one "low") to be of any interest. Since it
cannot be instantiated with only one domain, the example theorems in
Example_Valid_StateH now assume that `1 <= maxDomain`.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
For CRefine, this process is much more complex than for Refine and up,
as the C code both has its own definitions `maxDom` and `numDomains`,
but they are not defined in terms of each other, only numbers.
Similarly, array size types and their corresponding ArrayGuard bounds
checks refer to specific numbers, making a fullproof abstraction impossible.
A reasonably constrained interface to numDomains/maxDomain/maxDom in
Wellformed_C provides a sufficient abstraction to allow the proofs to be
independent of the number of domains (constrained to <= 256). Using the
value_type command allows more abstraction techniques, such as linking
the size of the scheduler queues back to numDomains*numPriorities,
without stating what the numbers are. Finally, for getting past the
ArrayGuard bounds checks, we do leak some information in the form of
`explicit` lemmas. These are the least safe, but short of augmenting the
C parser to re-wrap array sizes into equivalent constants/types, they
constitute a limited risk. Nonetheless, `explicit` lemmas should be used
as sparingly as possible.
Refinement to C proceeds by pretending we don't know the number of
domains, and whenever a control flow decision is made based on
`numDomains > 1`, we follow both branches, as we did for Refine. We also
attempt to avoid clever rewrites such as `(x < 1) = (x = 0)` which mess
up bounds checks into a domain-size array when `numDomains = 1`.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Proofs now don't care about numDomains, except for a small interface in
Invariants_H. The interface is currently by convention only, and has no
enforcement capabilities.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The proofs work without knowing the number of domains, including with
only a single domain.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Make proofs work with any number of domains that fits in the domain type
(at this time an 8-bit word).
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Introduce Kernel_Config theory for storage of non-architecture-specific
seL4 configuration variables that are shared by the abstract and design
specs.
Remove `num_domains`, in lieu of `numDomains` that is now defined only
in `Kernel_Config.thy`. The definition is hidden and must be referred to
as Kernel_Config.numDomains_def when avoiding unfolding is not possible.
Include required properties of `numDomains` as lemmas.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The `value_type` top-level command allows evaluating a term down to a
natural number, and using that number to define an enumerated type, as
well as (optionally) a constant definition.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This link is stable over Isabelle releases and can be updated once
the repo switches over to the next release.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The new docker containers that upgraded to gcc-10 use a different
version of the gcc Arm toolchain (`arm-linux-gnueabi`).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The aim of the PR was readability, but it actually also brings the
C more in line with the spec.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
In the rest of the proofs we use machine_word to refer to addresses.
This commit brings the machine definitions in line with that.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Matthew Brecknell
Michael McInerney
Michael McInerney
Rafal Kolanski
Corey Lewis
Gerwin Klein
Ryan Barry