Formal Method
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, and implement robust cryptographic techniques tested on a trusted microcontroller to ensure only authorized users can initiate the boot process.
The correctness ( formal verification) of the PIT security protocol is verified using Coloured-Petri Nets (CPN). We use a threat modeling framework, STRIDE to demonstrate various cyber-attacks through the CPN.
Firmware like the Basic Input Output System (BIOS) is essential for a computing device's operation, as it facilitates communication between the hardware and the operating system. However, firmware is vulnerable to unauthorized and malicious modifications, which are particularly serious because they allow attackers to gain full control over the entire computing system, effectively bypassing all security measures of the operating system and higher layers. Although there are industry protocols to secure the boot process, firmware remains easy to tamper with once the device is running. This issue is especially critical when devices are transported, as they can be intercepted and booted by malicious actors. To mitigate this threat, we have developed the Protection in Transit (PIT) protocol, which locks the device during transit and ensures that only authorized users can boot it up. Given the crucial role of the PIT protocol in device security, it is imperative to provide formal guarantees of its correctness and security. This paper enhances the PIT protocol in two significant ways. First, we validate its correctness using Coloured Petri Nets (CPN) and demonstrate its robustness against potential cyberattacks through Microsoft's STRIDE threat modeling framework. We then incorporate the findings from the STRIDE analysis into the CPN model to assess the PIT protocol's security, thereby increasing confidence in its ability to protect devices during transit. Second, we delve into the core functionalities of the PIT protocol by developing implementation libraries that utilize robust cryptographic techniques. These techniques have been rigorously tested on a trusted microcontroller.