Tipo di tesi
Tesi di laurea magistrale
Titolo
Formal verification of security properties in the MSP430 microcontroller
Corso di studi
INFORMATICA
Parole chiave
- Coq
- cybersecurity
- formal methods
- ISA
- Katamaran
- MSP430
- Rocq
- verification
Data inizio appello
18/07/2025
Riassunto (Italiano)
Instruction set architectures often promise some security property, but then fail to uphold it in their functional specification. Formal methods can be applied to eliminate the possibility of such inconsistencies and the associated vulnerabilities. In recent years, the availability of machine-readable architectural specifications has sparked the development of tools that aid proofs on ISAs. Katamaran is one such tool. We verify security properties of the MSP430, a microcontroller with wide commercial adoption, demonstrating the applicability of Katamaran to real-world architectures.
