b00t-c0d3

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.

Verified

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

Attacks (each has their own branch)

• Attack Fail Function
• Attack Image Length
• Attack PMP
• Attack OTBN (no vulnerability detectable)
• Attack Hash/HMAC
• Attack Whitelist Tamper
• Attack Whitelist Fail Functions