Since the advent of Spectre attacks, researchers and practitioners have developed a range of hardware and software measures to counter transient execution attacks. A prime example of such mitigation is speculative load hardening (slh) in LLVM, which protects against leaks by tracking the speculation state and masking values during misspeculation. LLVM relies on static analysis to harden programs using slh that often results in over-protection, which incurs performance overhead. We extended an existing side-channel model validation framework, Scam-V, to check the vulnerability of programs to Spectre-PHT attacks and optimize the protection of programs using the slh approach. We illustrate the efficacy of Scam-V by first demonstrating that it can automatically identify Spectre vulnerabilities in programs, e.g., fragments of crypto-libraries. We then develop an optimization mechanism to validate the necessity of slh hardening w.r.t. the target platform. Our experiments showed that hardening introduced by LLVM in most cases could be improved when the underlying microarchitecture properties are considered.

With the increasing ubiquity of computing devices, their correct and secure operation is of growing importance. In particular, critical components that provide core functionalities or process sensitive data have to operate as intended. Examples are operating systems that must provide proper isolation among applications, device drivers that must reliably communicate with the hardware, crypto routines that must avoid leakage of sensitive information, and low-level security mechanisms that must be implemented correctly to be effective. All these make use of hardware functionalities that are beyond plain software execution. Therefore, they should ideally be verified at binary level to accurately account for the effects their execution has on the underlying hardware systems.

Verifying properties of binary code is challenging because of its lack of structure in terms of control flows and memory representations, and the complex hardware specifics involved. In this thesis, we aim to improve the precision and trustworthiness of binary code analyses by basing the analyses on interactive theorem proving. We contribute with the new HolBA framework for binary analysis, which is built on top of the HOL4 theorem prover. This allows all implemented algorithms to produce machine-checked correctness proofs for their results. We applied this to implement translation procedures into the intermediate language BIR to facilitate analyses. The proof-producing analysis procedures we provide for program verification are the weakest precondition propagation and symbolic execution. We evaluated the framework with a number of binaries and a larger case study, which is the control software for a balancing robot. The latter has been used as an analysis target to establish execution time bounds using symbolic execution.

Since verification is carried out on models of hardware, the applicability of the verification results hinges on how well the used models reflect the actual hardware. In particular, in the context of security applications, where an attacker tries to exploit traits of hardware execution, this has received less attention in the formal methods community. We contribute with the new Scam-V methodology and tool for differential testing to discover possible instances where the attacker-exploitable behavior of a model and a real hardware system diverge. In a number of case studies with real processors, we found a number of new types of leakage that could be exploited by an attacker. Additionally, our validation exercises revealed a number of modeling issues.

Med datorer och inbyggda system förekommande överallt i dagens samhälle blir dessas korrekthet och säkerhet allt viktigare. I synnerhet måste mjukvarukomponenter som bidrar med viktig funktionalitet eller hanterar känslig data fungera som avsett. Exempel på komponenter är operativsystem som måste isolera applikationer, drivrutiner som måste kommunicera med hårdvaran på ett tillförlitligt sätt, kryptografiska rutiner som inte får läcka känslig information och fundamentala säkerhetsmekanismer vars resultat beror starkt på implementationens korrekthet. Alla dessa komponenter involverar hårdvaruaspekter som normalt sett inte involveras vid exekvering av applikationsprogram. För korrekt verifiering bör därför dessa komponenter analyseras på binär nivå.

Att verifiera binärkodsegenskaper är utmanande då kontrollflöden och minnesrepresentationer saknar struktur i binärkod, och för att verifieringen involverar komplexa hårdvarudetaljer. I denna avhandling förbättrar vi precisionen och tillförlitligheten i binärkodsanalys med hjälp av en interaktiv bevisassistent. Vi presenterar ramverket HolBA för binärkodsanalys, som vi har implementerat i den interaktiva bevisassistenten HOL4. HolBA möjliggör implementation av analysalgoritmer så att algoritmerna producerar maskinkontrollerade korrekthetsbevis för dessas beräknade resultat. Vi har använt HolBA för att implementera översättningsprocedurer från binärkod till det mer abstrakta programspråket BIR för att underlätta formell analys. HolBA har två bevisproducerande analysrutiner för att möjliggöra programverifiering: en rutin för symbolisk exekvering och en rutin som beräknar det minst restriktiva villkoret som garanterar att programets resultat satisfierar ett givet villkor. Vi utvärderar HolBA med hjälp av ett antal binära program, och en större fallstudie bestående av ett program som styr en självbalanserande robot. Robotmjukvarans exekveringstider har analyserats med symbolisk exekvering för att verifiera dess övre och undre tidsgränser.

Verifieringsresultatens tillförlitlighet beror på hur precist hårdvarumodellerna återspeglar den faktiska hårdvaran. Denna aspekt har fått begränsad uppmärksamhet i samband med säkerhet, där subtila hårdvaruoperationer kan utnyttjas vid angrepp. Vi presenterar Scam-V, en metod och ett verktyg för differentiell testning, som upptäcker skillnader i beteende mellan modell och hårdvara som kan ge upphov till säkerhetssårbarheter. I ett antal fallstudier med riktiga processorer hittades, tidigare okända, typer av informationsläckage.

Observational models enable the analysis of information flow properties against side channels. Relational testing has been used to validate the soundness of these models by measuring the side channel on states that the model considers indistinguishable. However, unguided search can generate test states that are too similar to each other to invalidate the model. To address this we introduce observation refinement, a technique to guide the exploration of the state space to focus on hardware features of interest. We refine observational models to include fine-grained observations that characterize behavior that we want to exclude. States that yield equivalent refined observations are then ruled out, reducing the size of the space. We have extended an existing model validation framework, Scam-V, to support refinement. We have evaluated the usefulness of refinement for search guidance by analyzing cache coloring and speculative leakage in the ARMv8-A architecture. As a surprising result, we have exposed SiSCLoak, a new vulnerability linked to speculative execution in Cortex-A53.

Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found. We introduce the novel Hoare-style program logic , which interprets postconditions relative to program points when these are first encountered. The logic can support both partial and total correctness, derive contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of  have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, making it applicable to the ARMv6 and ARMv8 instruction sets.

Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs which invalidate the models due to hidden microarchitectural behavior.

Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a common design: the adoption of hardware-independent intermediate representations, a mechanism to translate architecture dependent code to this representation, and a set of architecture independent analyses that process the intermediate representation. The usage of these platforms to verify software introduces the need for trusting both the correctness of the translation from binary code to intermediate language (called transpilation) and the correctness of the analyses. Achieving a high degree of trust is challenging since the transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encodings (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). Similarly, analyses can use complex transformations (e.g. loop unrolling) and simplifications (e.g. partial evaluation) of the artifacts, whose bugs can jeopardize correctness of the results. We overcome these problems by developing a binary analysis platform on top of the interactive theorem prover HOL4. First, we formally model a binary intermediate language and we prove correctness of several supporting tools (i.e. a type checker). Then, we implement two proof-producing transpilers, which respectively translate ARMv8 and CortexM0 programs to the intermediate language and generate a certificate. This certificate is a HOL4 proofdemonstrating correctness of the translation. As demonstrating analysis, we implement a proof-producing weakest precondition generator, which can be used to verify that a given loop-free program fragment satisfies a contract. Finally, we use an AES encryption implementation to benchmark our platform.

In order to handle the complexity and heterogeneity of modern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent intermediate representations. The usage of these platforms to verify systems down to binary-level is appealing due to the high degree of automation they provide. However, it introduces the need for trusting the correctness of the translation from binary code to intermediate language. Achieving a high degree of trust is challenging since this transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encoding (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). We overcome these problems by formally modeling one of such intermediate languages in the interactive theorem prover HOL4 and by implementing a proof-producing transpiler. This tool translates ARMv8 programs to the intermediate language and generates a HOL4 proof that demonstrates the correctness of the translation in the form of a simulation theorem. We also show how the transpiler theorems can be used to transfer properties verified on the intermediate language to the binary code.

Embedded systems for critical applications are typically specified with requirements on predictable timing and safety. While ensuring predictable timing, the RTFM-lang (Real-Time For the Masses) model of computation (MoC) currently lacks memory access protection among real-time tasks. In this paper, we discuss how to safely verify task execution given a specification using the RTFM-MoC. Furthermore, an extension to the RTFM-core infrastructure is outlined and tested with use cases of embedded development. We propose a method for run time verification exploiting memory protection hardware. For this purpose, we introduce memory resources to the declarative language RTFM-core allowing compliance checks. As a proof of concept, compiler support for model analysis and automatic generation of run time verification code is implemented together with an isolation layer for the RTFM-kernel. With this verification foundation, functional run time checks as well as further overhead assessments are future research questions.

Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found.We introduce the novel Hoare-style program logic L_a, which interprets postconditions relative to program points when these are first encountered. The logic supports both partial and total correctness, derives contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of L_a have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, which supports the ARMv6, ARMv8 and RISC-V instruction sets.