Overview
Enhancing the Protection in Transit (PIT) protocol—which locks devices during transit to prevent unauthorized firmware tampering—we formally verify its correctness and security using Coloured Petri Nets and the STRIDE threat modeling framework. We implement robust cryptographic techniques on a trusted microcontroller to ensure only authorized users can initiate the boot process.
Research Objectives
- Formally verify correctness of the PIT protocol using Coloured Petri Nets (CPN).
- Analyze security robustness against cyber threats using Microsoft's STRIDE model.
- Integrate cryptographic techniques into trusted microcontrollers for secure deployment.
- Demonstrate protocol’s resilience against firmware attacks during transit.
Methods
The correctness of the PIT security protocol is verified using Coloured-Petri Nets (CPN). We use STRIDE threat modeling to demonstrate potential attacks on firmware. The CPN model is further enhanced based on STRIDE insights to verify robustness. We also implement PIT functionality using strong cryptographic libraries on trusted microcontrollers to ensure end-to-end secure operation.
Results & Visualizations
Impact
Firmware such as BIOS is a crucial component of device security but remains vulnerable to tampering. The PIT protocol provides a trusted mechanism for securing devices in transit and preventing unauthorized firmware execution. Our formal verification work ensures strong guarantees about PIT’s correctness and resilience. In addition, the implementation of cryptographic protections on trusted microcontrollers provides a practical path to wide-scale adoption of PIT in secure supply chains.