The goal is to verify the security of the boot code using CBMC
mask_rom_boot_code.c contains the unaltered boot code without annotations. The boot code is inspired by the OpenTitan's secure boot pseudocode and specification. The unaltered boot code can be found at https://github.com/KVISDAOWNER/b00t-c0d3.
A description of the properties can be found in properties.pdf.
- Property 1
- Property 2
- Property 3
- Property 4
- Property 5
- Property 6
- Property 7
- Property 8
- Property 9
- Property 10
- Attack Fail Function
- Attack Image Length
- Attack PMP
- Attack OTBN (no vulnerability detectable)
- Attack Hash/HMAC
- Attack Whitelist Tamper
- Attack Whitelist Fail Functions