Skip to content

Latest commit

 

History

History
27 lines (23 loc) · 824 Bytes

README.md

File metadata and controls

27 lines (23 loc) · 824 Bytes

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