1. Towards a Trustworthy Stack: Formal Verification of Low-Level Hardware and Software
- Author
-
Dong, Ning and Dong, Ning
- Abstract
Computer systems, consisting of hardware and software, have gained significant importance in the digitalised world. These computer systems rely on critical components to provide core functionalities and handle sensitive data. A fundamental requirement for these critical components is functional correctness, which ensures that the components work as their specifications prescribe. For instance, a pipelined processor will execute instructions concurrently in different stages such as fetch, decode and execute, and must produce results as specified in the instruction set architecture (ISA) manual. In addition to functional correctness, security properties such as confidentiality and integrity are important. In particular, confidentiality requires that sensitive data is only accessible to authorised users. To construct a correct and secure computer (i.e., a trustworthy stack), this thesis focuses on the functional correctness and confidentiality of peripherals and pipelined processors using the HOL4 interactive theorem prover. For functional correctness, we use a refinement-based verification approach where the execution of a target system is constrained by a reference system. We have studied this for two different target systems, a synchronous serial peripheral interface (SPI) device along with its driver, and a 5-stage pipelined processor. Specifically, we formalise an SPI device and its driver, and present an abstract model as the reference system. The abstract model ensures correct communications in the SPI half- and full-duplex modes. The refinement between the abstract and SPI models is established using weak bisimulation. Secondly, we implement and verify a 5-stage in-order pipelined processor Silver-Pi for the RISC ISA Silver. The correctness of Silver-Pi is proved by exhibiting a refinement relation between the traces of the processor and the Silver ISA. Silver-Pi is implemented using the verified HOL4 Verilog library, which ensures the correctness of the proces, Datorsystem, bestående av hårdvara och mjukvara, har fått stor betydelse i den digitaliserade världen.Dessa datorsystem är beroende av kritiska komponenter för att tillhandahålla grundläggande funktionalitet och hantera känslig information. Ett grundläggande krav för dessa kritiska komponenter är funktionell korrekthet, vilket säkerställer att komponenterna fungerar som deras specifikationer föreskriver. Till exempel kommer en pipelineprocessor att exekvera instruktioner samtidigt i olika steg, till exempel hämtning, dekodning och utförande, och måste producera resultat som specificeras i instruktionsuppsättning (ISA) manualen. Utöver funktionell korrekthet är säkerhetsegenskaper som konfidentialitet och integritet också viktiga. Särskilt kräver konfidentialitet att känslig information endast är tillgänglig för auktoriserade användare. För att konstruera en korrekt och säker dator (dvs. en pålitlig stack), fokuserar denna avhandling på den funktionella korrektheten och konfidentialiteten hos periferiutrustningar och pipelined-processorer med hjälp av det interaktiva bevisprogrammet HOL4. För funktionell korrekthet använder vi ett verifieringssätt baserat på för-fining där utförandet av ett målsystem begränsas av ett referenssystem. Vi har studerat detta för två olika målsystem, en synkron seriell peripheral interface (SPI) tillsammans med dess drivrutin, och en 5-stegs pipelined processor. Specifikt formaliserar vi en SPI-anordning och dess drivrutin, och presenterar en abstrakt modell som referenssystemet. Den abstrakta modellen säkerställer korrekt kommunikation i SPI:s halv- och hel-duplexlägen. Förfiningen mellan den abstrakta och SPI-modellerna fastställs med hjälp av svag bisimulering. För det andra implementerar och verifierar vi en 5-stegs in-order pipelined processor Silver-Pi för RISC ISA Silver. Korrektheten hos Silver-Pi bevisas genom att uppvisa ett förfiningsförhållande mellan processorernas exkveringsspår och Silver ISA.Silver-Pi är implementerad med, QC 20231221
- Published
- 2024