Tesi etd-06172025-225931 |
Link copiato negli appunti
Tipo di tesi
Tesi di laurea magistrale
Autore
DUE', ALESSIO
URN
etd-06172025-225931
Titolo
Formal verification of security properties in the MSP430 microcontroller
Dipartimento
INFORMATICA
Corso di studi
INFORMATICA
Relatori
relatore Prof. Ferrari, Gian Luigi
Parole chiave
- Coq
- cybersecurity
- formal methods
- ISA
- Katamaran
- MSP430
- Rocq
- verification
Data inizio appello
18/07/2025
Consultabilità
Completa
Riassunto
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.
File
| Nome file | Dimensione |
|---|---|
| final_digital.pdf | 745.05 Kb |
Contatta l’autore |
|