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.