Proving Safety and Security of Binary Programs

التفاصيل البيبلوغرافية
العنوان:	Proving Safety and Security of Binary Programs
بيانات النشر:	KTH, Teoretisk datalogi, TCS Stockholm 2023
تفاصيل مُضافة:	Lindner, Andreas
نوع الوثيقة:	Electronic Resource
مستخلص:	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 Med datorer och inbyggda system förekommande överallt i dagens samhälle blir dessas korrekthet och säkerhet allt viktigare. I synnerhet måste mjukvarukomponenter som bidrar med viktig funktionalitet eller hanterar känslig data fungera som avsett. Exempel på komponenter är operativsystem som måste isolera applikationer, drivrutiner som måste kommunicera med hårdvaran på ett tillförlitligt sätt, kryptografiska rutiner som inte får läcka känslig information och fundamentala säkerhetsmekanismer vars resultat beror starkt på implementationens korrekthet. Alla dessa komponenter involverar hårdvaruaspekter som normalt sett inte involveras vid exekvering av applikationsprogram. För korrekt verifiering bör därför dessa komponenter analyseras på binär nivå. Att verifiera binärkodsegenskaper är utmanande då kontrollflöden och minnesrepresentationer saknar struktur i binärkod, och för att verifieringen involverar komplexa hårdvarudetaljer. I denna avhandling förbättrar vi precisionen och tillförlitligheten i binärkodsanalys med hjälp av en interaktiv bevisassistent. Vi presenterar ramverket HolBA för binärkodsanalys, som vi har implementerat i den interaktiva bevisassistenten HOL4. HolBA möjliggör implementation av analysalgoritmer så att algoritmerna producerar maskinkontrollerade korrekthetsbevis för dessas beräknade resultat. Vi har använt HolBA för att implementera översättningsprocedurer från binärkod till det mer abstrakta programspråket BIR för att underlätta formell analys. HolBA har två bevisproducerande analysrutiner för att möjliggöra programverifiering: en rutin för symbolisk exekvering och en rutin som beräknar det minst restriktiva villkoret som garanterar att programets resultat satisfierar ett givet villkor. Vi utvärderar HolBA med hjälp av ett antal binära program, och en större fallstudie bestående av ett program som styr en självbalanserande robot. Robotmjukvarans exekveringstider har analyserats med symbolisk exekvering för att verifiera dess övre och undre QC 20230509
مصطلحات الفهرس:	Binary Code, Binary Analysis, Formal Verification, Model-Based Testing, Theorem Proving, HOL4, Intermediate Language, Instruction Set Architectures, ISA, Observational Models, Symbolic Execution, Weakest-Precondition, Execution Time Analysis, binärkod, binärkodsanalys, formell verifiering, modellbaserad testning, satsbevisning, mellankod, instruktionsuppsättningar, observationsmodeller, symbolisk exekvering, minst restriktiva villkoret, analys av övre tidsgräns, Computer Sciences, Datavetenskap (datalogi), Doctoral thesis, comprehensive summary, info:eu-repo/semantics/doctoralThesis, text
URL:	http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-326719 TRITA-EECS-AVL ; 2023:41
الإتاحة:	Open access content. Open access content info:eu-repo/semantics/openAccess
ملاحظة:	application/pdf English
أرقام أخرى:	UPE oai:DiVA.org:kth-326719 0000-0001-5311-1781 urn:isbn:978-91-8040-583-6 1382497152
المصدر المساهم:	UPPSALA UNIV LIBR From OAIster®, provided by the OCLC Cooperative.
رقم الأكسشن:	edsoai.on1382497152
قاعدة البيانات:	OAIster

الوصف
الوصف غير متاح.