The SimplExportAndRefine session is one of the steps of binary
verification and only available for ARM and RISCV64.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This action will run the C proofs when the label `proof-test` is added
to a pull request. Intended to be used when the preprocess test has
failed and the PR is ready to check proofs.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The top phys addr is exclusive, not inclusive. On 64-bit platforms there
is a trivial way to fix this as long as the whole address space is never
used. For 32-bit platforms the fix will be more complicated, so this is
postponed.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
This adds support for the ODroidC4. The ODroidC4 is just a beefier
ODroidC2 with some bits moved around. The devices we care about here are
all essentially the same except the cores are A55s instead of A53s.
Signed-off-by: Curtis Millar <curtis@curtism.me>
This adds basic support for the ARM Cortex A55 cpu core as is used in
the Amlogic S905x3 that is found in the ODroid C4.
Signed-off-by: Curtis Millar <curtis@curtism.me>
Also make the output more verbose in case of errors, which is
helpful when porting the kernel to new platforms.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Add underscored in name to improve readability.
- Add brackets to ensure parameters are atoms
- add comment clarifying c99 usage
Signed-off-by: Axel Heider <axelheider@gmx.de>
Currently only for GitHub actions (but these will be replacing Bamboo
tests in the coming weeks).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The flags argument means that the call requires 2 time args (period,
budget) and 3 words (extra refills, badge, flags).
Signed-off-by: Curtis Millar <curtis@curtism.me>
This adds a simple vulnerability disclosure policy, loosely based on:
- Disclose.io materials.
- The OWASP Vulnerability Disclosure Cheat Sheet.
Signed-off-by: Matthew Brecknell <matthew@brecknell.net>
This action runs the verification C parser on the main kernel
configurations to check that the code is in the C verification subset.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
With this change, even architectures which do not use a distinct region
to map the kernel ELF will use the `kpptr_to_addr` to translate any
address from the kernel region.
This ensures that these accesses are correctly checked for bounds when
used and will make it easier to move the ELF mapping into a distinct
region of virtual address space.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Move all of the virtual to physical translation functions into a single
common file and use the updated constants.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Only emit non-STATUS level messages if there is an error or significant
warning condition during build configuration.
Signed-off-by: Kent McLeod <kent@kry10.com>
According to the CMake documentation, this is intended for file
redirection. Since we don't redirect to files, but basically enforce
std channels, this conflicts with any existing redirection set up when
CMake is invoked. As a result the messages are lost.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
This will build a PDF of the reference manual in draft mode
and upload that PDF as a build artifact.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The old draftcopy package doesn't seem to work on newer texlive
installations. We also don't want to pass `draft` to the `report`
style, because that will switch off images.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
