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 processor down to its Verilog implementation. 

For the SPI case study, weak bisimulation ensures that the SPI model has the same information flows as the abstract model, which prevents malicious driver operations e.g., an infinite loop based on a secret value.

In general, to prevent secret leaks caused by phenomena such as instruction pipelining and out-of-order (OoO) execution, the target and reference systems are augmented by observations that extract visible parts of the machine state to attackers. This allows a variety of information channels based on e.g. timing and cache access behaviour to be captured. As a security policy, we use the notion of conditional noninterference (CNI), which guarantees that a target system does not leak more information than what the reference system allows.

In order to analyse the timing channel of Silver-Pi, the observation function extracts the parts of the ISA state that may affect the execution time of a program. With this reference system, we prove that Silver-Pi satisfies CNI.

For OoO execution, we present the formalisation of a machine independent language, MIL, which uses a small set of primitive events to describe both in-order and OoO execution at a microarchitecture-like level. A notion of CNI in MIL rules out trace-driven cache side channels by comparing OoO and in-order execution of a program. We present a semi-automated verification strategy for CNI using the executable semantics and demonstrate this strategy with several examples. The executable semantics computes results and generates observations during the execution of MIL programs.

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 det verifierade HOL4 Verilog-biblioteket, vilket säkerställer processorns korrekthet ner till dess Verilog-implementation.

För SPI-fallstudien säkerställer svag bisimulering att SPI-modellen har samma informationsflöden som den abstrakta modellen, vilket förhindrar skadliga drivrutinsoperationer, t.ex. en oändlig loop baserad på ett hemligt värde.

I allmänhet, för att förhindra läckage av hemligheter orsakade av fenomen som instruktionspipelining och omordnad (OoO) exekvering, kompletteras mål- och referenssystemen med observationer som extraherar synliga delar av maskinens tillstånd för angripare. Detta möjliggör att en mängd informationskanaler baserat på exempelvis tid och cacheåtkomstbeteende kan fångas upp. Som säkerhetspolicy använder vi begreppet konditionell icke-interferens (CNI), vilket garanterar att ett målsystem inte läcker ut mer information än vad referenssystemet tillåter.

För att analysera tidkanalen hos Silver-Pi, extraherar observationsfunktionen delar av ISA-tillståndet som kan påverka exekveringstiden för ett program.Med detta referenssystem bevisar vi att Silver-Pi uppfyller CNI.

För OoO-utförande presenterar vi formaliseringen av ett maskinoberoende språk, MIL, som använder en liten uppsättning primitiva händelser för att beskriva både in-order och OoO-utförande på en mikroarkitekturliknande nivå. Ett begrepp av CNI i MIL utesluter spårdrivna cache-sidokanaler genom att jämföra OoO och in-order utförande av ett program. En verifierad körbar semantik beräknar resultat och genererar observationer av MIL-program. Vi presenterar en semi-automatiserad verifieringsstrategi för CNI med hjälp av den körbara semantiken och demonstrerar denna strategi med flera exempel.