Add cheriot-audit docs & exercises
#46
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
AlexJones0
force-pushed
the
audit_exercises
branch
from
04e9f05
to
23ed0ad
Compare
HU90m
requested changes
Sep 24, 2024
Adds a basic document giving an introduction to `cheriot-audit`, a short guide to setting it up, a brief introduction to using it, and pointers to appropriate upstream sources of documentation. This also includes a quick primer on Rego, with an introduction to some of the language's features and syntax.
AlexJones0
force-pushed
the
audit_exercises
branch
from
23ed0ad
to
3420747
Compare
HU90m
approved these changes
Sep 25, 2024
This commit introduces exercise 1 for using CHERIoT Audit to audit firmware alongside Rego policies. This exercise involves writing a policy to detect if firmware uses sealed capabilities, and to query information about these capabilities if they exist.
This commit introduces exercise 2 for using CHERIoT Audit to audit firmware alongside Rego policies. This exercise involves writing a policy to ensure that only specified functions are running with interrupts disabled.
This commit introduces exercise 3 for using CHERIoT Audit to audit firmware alongside Rego policies. This exercise involves writing a policy to ensure that specific allocation limits are respected, with individual allocation limits per allocation capability, per compartment (total) and across all compartments.
AlexJones0
force-pushed
the
audit_exercises
branch
from
3420747
to
dc260cc
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds documentation/exercises for
cheriot-auditand OPA Rego (the language it uses).A short documentation page on auditing firmware is introduced - this primarily provides a link to documentation sources (for CHERIoT Audit and Rego), an introduction to what CHERIoT Audit is used for, a guide to setting up and using
cheriot-audit, as well as some basic recommendations for Rego development.3 self-contained exercises are then introduced, alongside a quick introduction/primer explaining some basic concepts/syntax in Rego to enable readers to follow the exercises. The exercises are as follows:
Note that this PR is made based on my understanding of CHERIoT Audit / Rego solely from some initial experimentation and developing these three exercises. As such, there may be some instances where wording is not entirely accurate or best practices are not being followed. I have mainly focused on creating and documenting some working examples, to be able to showcase what kind of things are possible when auditing firmware.