restructure how verified configs are displayed#306
Conversation
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
| - integrity and availability (access control) | ||
| - confidentiality (information flow) | ||
| - binary correctness, covering C functions that have C-level verification | ||
| - user-level system initialisation |
There was a problem hiding this comment.
What is meant with this? Setting up the initial task?
There was a problem hiding this comment.
Verification of the capDL initialiser root task (on the model level, there is no C-level proof at the moment, although there was a binary-level proof via CakeML for a while that never really made it into production).
There was a problem hiding this comment.
Have added more explanation now that there is space (previously this was all very contracted and probably not useful).
There was a problem hiding this comment.
Hm, but capDL isn't part of the seL4 kernel, so somewhat strange to mention it here, especially as it should be pretty much platform independent.
There was a problem hiding this comment.
It's part of the proof stack and it is very architecture dependent (but largely platform independent inside AArch32, although sensitive to things like FPU on/off etc).
|
Is there a way to check the rendered result? I tried downloading the artifact, but that wasn't very useful. |
lsf37
force-pushed
the
verified-configs
branch
from
899b882 to
279008c
Compare
Unfortunately not from the GitHub interface, you'd have to clone and build locally to browse it or point a web server at the generated artefact. |
- each hardware platform now declares a list of verified configs (empty if no verification, one or more of ARM, ARM_HYP, AARCH64, RISCV64, X64 otherwise; can be extended with other tags, only needs a corresponding section on verified configs page) - verified configs page has a section for each main config class, lists all platforms for that class - platforms page produces a tick if any verified config is present and links to the verified configs each platform enumerates Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
lsf37
force-pushed
the
verified-configs
branch
from
279008c to
bd81ede
Compare
2 participants
each hardware platform now declares a list of verified configs (empty if no verification, one or more of ARM, ARM_HYP, AARCH64, RISCV64, X64 otherwise; can be extended with other tags, only needs a corresponding section on verified configs page)
verified configs page has a section for each main config class, lists all platforms for that class
platforms page produces a tick if any verified config is present and links to the verified configs each platform enumerates