This work investigates possible improvements to an existing annotation inference tool. The tool is part of a toolchain that aims to automate the process of software verification using formal methods. The purpose of the annotations is to facilitate the use of deductive verification, which is the formal method used in this project for proving that a given program meets its specifications. In the project, two categories of annotations are established. The first category is the category of functional annotations. These annotations describe the behavior of a function or a module. The other category is what we call auxiliary annotations. These annotations describe properties that are necessary for proving the correctness of the functional annotations. The tool that this work tries to improve is dedicated to inferring the auxiliary annotations. To our knowledge, this is the first tool of its kind to automatically infer auxiliary annotations for a complete module given the module’s source code and its interface specifications. The work contributed in four areas: inferring annotations from the interface specifications of a module and propagating these annotations to all the helper functions used in the module; inferring annotations for floating-point constructs; inferring annotations for pointer constructs; and finally, inferring annotations for array constructs. The improved tool was tested on production embedded code used in the heavy automotive industry. The results demonstrated a considerable improvement and were in line with earlier findings. The work confirms the feasibility and usability of auxiliary annotation inference in this scope. / Detta arbete undersöker möjliga förbättringar av ett befintligt verktyg för härledning av annoteringar (annotations). Verktyget är en komponent i en verktygskedja som syftar till att automatisera processen för mjukvaruverifiering med formella metoder. Syftet med annoteringarna är att underlätta användningen av deduktiv verifiering, vilket är den formella metod som används i detta projekt för att bevisa att ett givet program uppfyller dess specifikationer. I projektet fastställs två kategorier av annoteringar. Den första kategorin är kategorin funktionella annoteringar. Dessa annoteringar beskriver beteendet hos en funktion eller en modul. Den andra kategorin är vad vi kallar hjälp annoteringar (auxiliary annotations). Dessa annoteringar beskriver egenskaper som är nödvändiga för att bevisa korrektheten av de funktionella annoteringarna. Verktyget som detta arbete försöker förbättra är dedikerat till att härleda hjälp annoteringar. Arbetet bidrog inom fyra områden: att härleda annoteringar från gränssnittsspecifikationerna (interface specifications) för en modul och sprida dessa annoteringar till alla hjälpfunktioner som används i modulen; härleda annoteringar för flyttalskonstruktioner (floating-point constructs); härleda annoteringar för pekarkonstruktioner; och slutligen, härleda annoteringar för arraykonstruktioner. Det förbättrade verktyget testades på produktionsinbyggdad kod som används inom fordonsindustrin. Resultaten visade en avsevärd förbättring och var i linje med tidigare resultat. Arbetet bekräftar genomförbarheten och användbarheten av hjälpannoteringshärledning i projektets omfattning.

The most performant Machine Learning (ML) classifiers have been labeled black-boxes due to the complexity of their decision process. eXplainable Artificial Intelligence (XAI) methods aim to alleviate this issue by crafting an interpretable explanation for a models prediction. A drawback of most XAI methods is that they are heuristic with some drawbacks such as non determinism and locality. Formal Explanations (FE) have been proposed as a way to explain the decisions of classifiers by extracting a set of features that guarantee the prediction. In this thesis we explore these guarantees for different use cases: speeding up the inference speed of tree-based Machine Learning classifiers, curriculum learning using said classifiers and also reducing training data. We find that under the right circumstances we can achieve up to 6x speedup by partially compiling the model to a set of rules that are extracted using formal explainability methods. / De mest effektiva maskininlärningsklassificerarna har betecknats som svarta lådor på grund av komplexiteten i deras beslutsprocess. Metoder för förklarbar artificiell intelligens (XAI) syftar till att lindra detta problem genom att skapa en tolkbar förklaring för modellens prediktioner. En nackdel med de flesta XAI-metoder är att de är heuristiska och har vissa nackdelar såsom icke-determinism och lokalitet. Formella förklaringar (FE) har föreslagits som ett sätt att förklara klassificerarnas beslut genom att extrahera en uppsättning funktioner som garanterar prediktionen. I denna avhandling utforskar vi dessa garantier för olika användningsfall: att öka inferenshastigheten för maskininlärningsklassificerare baserade på träd, kurser med hjälp av dessa klassificerare och även minska träningsdata. Vi finner att under rätt omständigheter kan vi uppnå upp till 6 gånger snabbare prestanda genom att delvis kompilera modellen till en uppsättning regler som extraheras med hjälp av formella förklaringsmetoder.

Application Specific Integrated Circuits (ASIC) and Field Programmable Gate Arrays (FPGA) verification is quite a time consuming phase in design flow cycle and it can be done using methodologies such as Universal Verification Methodology (UVM) and formal verification.The UVM methodology is simulation based verification where in the verifier will have to trigger the Design Under Test (DUT) manually by writing sequences which target different features of the DUT and the verification environment can also have verification directives such as assertions to spot design bugs. Formal verification on the other hand is purely assertion based verification where we describe the expected DUT behaviour using System Verilog Assertion (SVA) and we check for design sanity by exercising the assertions by letting the formal tool drive the inputs to the design in a constrained way. This completely eliminates the need of having to define sequences to drive the inputs. This thesis will bring up formal verification using jasper gold to light and will help verifiers to decide on how much of formal verification methodology can be used in verification of an IP with respect to the complexity of the design and the design behaviour to be verified. The results from this thesis proves how efficient formal verification was with respect to simulation based verification, to stress the design to test for corner case behaviour. The reason why formal verification cannot be extended for Top-Level Verification (TLV) and end to end functional verification is because of design complexity and this was also explored with the help of a complex ethernet design. Finally, a guideline as to when to use simulation based verification and formal verification was formulated. / ASIC och FPGA verifiering är en största del och är en tidskrävande fas av desingflödescyckeln. Det kan man göra den genom UVM eller Formell verifiering metoder.UVM metoder är simulering baserad verifiering där verifieraren måste utlösa DUT genom att skriva sekvenser som rikta olika funktioner av DUT och verifiering miljöer kan också ha verifiering direktiv som assertions som kan upptäcka designbugs.Formal verifiering är en assertion baserad verifiering metoder där i man kan beskriva förväntad DUT uppträdandet genom system verilog assertions (SVA) och verifiera designen genom använder assertions genom att låta det formal driva ingångarna till designen på ett begränsat sätt.Detta eliminerar helt behovet av att behöva definiera sekvenser för att driva ingångarna. Denna examensarbetena kommer att beskriva om formell verifiering med jasper gold och kommer att hjälpa verifierar bestämma hur mycket av den formal verifiering metoden kan man användas för att verifiera en ASIC IP med avseende på komplexitet och design uppträdandet att vara verifierat. Resultaten från denna examensarbetena kommer att bevisa hur effektiv formell metoderna var med avseende på simulering metoder att stressa design och verifiera den för undantags fall.Den ändleding varför formell verifiering metoder kan inte användande för TLV och från början till slut funktion verifiering är på grund av design komplexitet.Detta har analyserats med hjälp av en komplex ethernet design.En riktlinje för när kan man använda simulering metoder och formal metoder var föreslagit.

Contract inference consists in automatically computing contracts that formally describe the behaviour of program functions. Contracts are used in deductive verification, which is a method for verifying whether a system behaves according to a provided specification. The Saida plugin in Frama-C is a contract inference tool for C code. This thesis explores an extension to the Saida plugin which allows support for pointers and heap allocations. The goal is to evaluate to what extent model checking tools can be used to infer contracts for deductive verification of programs that use pointers and heap allocations. This is done by proposing a translation strategy to convert contracts containing heap expressions, generated by the model checker TriCera, into ACSL, a specification language used by Frama-C. An implementation of this translation is evaluated using a set of verification tasks. The results demonstrate that the inferred contracts are sucient to verify simple code samples, including features such as recursion, aliasing, and manipulation of heap-allocated structs. However, the results also reveal cases where the contracts are too weak, although more information could be extracted in the translation. It is concluded that model checking tools can infer contracts for deductive verification of programs with pointers and heap allocations, but currently to a limited extent. Several improvements to the translation strategy are proposed for future work. / Kontrakthärledning består i att automatiskt härleda kontrakt, vilka formellt beskriver funktioners beteende i program. Kontrakt används för deduktiv verifiering, vilket är en metod för att verifiera huruvida ett system beter sig enligt en given specifikation. Pluginet Saida i Frama-C är ett verktyg för kontrakthärledning för C-kod. Denna avhandling undersöker en vidareutveckling av Saida som möjliggör stöd för pekare och heap-allokeringar. Målet är att utvärdera i vilken utsträckning modellprovningsverktyg kan användas för att härleda kontrakt för deduktiv verifiering av program som använder pekare och heap-allokeringar. Detta görs genom att presentera en översättningsstrategi för att konvertera kontrakt som involverar heaputtryck, genererade av modellkontrollverktyget TriCera, till ACSL, vilket är ett specifikationsspråk som används av Frama-C. En implementation av denna översättning utvärderas med hjälp av en samling verifieringsproblem. Resultaten visar att de härledda kontrakten är tillräckliga för att verifiera enkla verifieringsproblem, med koncept som rekursion, aliasing och manipulation av heap-allokerade structs. Resultaten visar även fall då kontrakten är för svaga, men där mer information skulle kunna utvinnas i ¨översättningen. Slutsatsen dras att modellprovningsverktyg kan härleda kontrakt för deduktiv verifiering av program med pekare och heap-allokeringar, men för närvarande i begränsad utsträckning. Flera förbättringar av översättningsstrategin föreslås för framtida vidareutveckling.

HolBA is a binary analysis library that can be used to formally verify binary programs using contracts. It is developed in the interactive theorem prover HOL4 to achieve a high degree of trust in verification, the result of verification is a machine-checked proof demonstrating its correctness. This thesis presents two proof-producing procedures. The first resolve indirect jumps in BIR, the binary intermediate language used in HolBA, given their possible targets. The second transfers contracts proved on resolved BIR programs without indirect jumps to the original ones containing indirect jumps. This allows the existing weakest precondition generator to automatically prove contracts on loop-free BIR fragments containing indirect jumps. The implemented proof-producing procedures were evaluated on a small binary program and generated synthetic BIR programs. It was found that the first proof-producing procedure is not very efficient, which could pose a problem when verifying large binary programs. Future work could include improving the efficiency of the first proof-producing procedure and integrate it with an external tool that automatically finds possible targets of indirect jumps. / HolBA är ett bibliotek för binär analys som kan användas för att formellt verifiera binära program med kontrakt. Det är utvecklat i den interaktiva teorembevisaren HOL4 för att åstadkomma en hög grad av tillit till verifiering, resultatet av verifiering är ett maskin-kontrollerat bevis som demonstrerar dess korrekthet. Detta arbete presenterar två bevis-producerande procedurer. Den första bestämmer indirekta hopp i BIR, den binära mellanliggande representationen som används i HolBA, givet deras möjliga mål. Den andra överför kontrakt bevisade för bestämda BIR program utan indirekta hopp till originalen med indirekta hopp. Detta möjliggör den existerande svagaste förutsättning generatorn att automatiskt bevisa kontrakt för sling-fria BIR fragment som innehåller indirekta hopp. De implementerade bevis-producerande procedurerna utvärderades med ett litet binärt program och med genererade syntetiska BIR program. Det visades att den första bevis-producerande proceduren inte är särskilt effektiv, vilket skulle kunna vara ett problem vid verifiering av stora binära program. Framtida arbete skulle kunna inkludera att förbättra effektiviteten för den första bevis-producerande proceduren och att integrera den med ett externt verktyg som automatiskt kan hitta de möjliga målen för indirekta hopp.

Formal analysis of security protocols is becoming increasingly relevant. In formal analysis, a model is created of a protocol or system, and propositions about the security of the model are written. A program is then used to verify that the propositions hold, or find examples of where they do not. This report uses formal methods to analyse the authentication aspect of a protocol that allows private individuals, enterprises, and systems to securely and asynchronously share sensitive data. Unpublished, early drafts of the protocol were studied and algorithms described in it were verified with the help of the formal verification tool Tamarin Prover. The analysis revealed two replay attacks. Improvements to the protocol were suggested based on this analysis. In later versions of the protocol, the improvements have been implemented by the protocol developers. / Det blir alltmer relevant med formell analys av säkerhetsprotokoll. I formell analys så skapas en modell av ett protokoll eller ett system, och påståenden om modellens säkerhet skrivs. Ett program används sedan för att verifiera att påståendena gäller, eller för att hitta exempel där de inte gäller. Den här rapporten avänder formella metoder för att analysera autentiseringsaspekten av ett protokoll som tillåter privatpersoner, företag och system att asynkront dela känslig information på ett säkert sätt. Opublicerade och tidiga utkast av protokollet studerades och de algoritmer som beskrivs i protokollet verifierades med hjälp av Tamarin Prover. Analysen avslöjade två återspelningsattacker. Förbättringar till protokollet föreslogs baserat på denna analys. I senare versioner har protokollutvecklarna implementerat förslagen.

Model checking is a formal verification technique for verifying temporal properties in state-transition models. The main problem with using model checking is the state explosion problem, where the number of states in the model can grow exponentially, making verification infeasible. Previous work has tried to mitigate the state explosion problem by representing code blocks as Hoare-logic contracts in an abstract state-transition model using the temporal logic TLA. This is achieved by treating the block as atomic. In order to ensure that the abstract state-transition model is faithful with respect to the temporal properties you want to verify, only some code blocks can be considered atomic. This thesis aims to answer how atomic code blocks can be identified atomically and evaluate their potential for reducing state space during model checking. We give a theoretical foundation of what it means for a code block to be considered as atomic in TLA. Moreover, we introduce a property that characterizes these atomic code blocks and presents an algorithm to identify them for sequential programs written in a subset of C. Experimental results demonstrate that the identification of atomic code blocks using our algorithm can be used to significantly reduce the state space during model checking, with an average reduction factor of 62. The potential of this verification approach is promising, however, further case studies are necessary to better understand the extent of this reduction across different program types and properties. / Modellkontroll är en formell verifieringsteknik för att bekräfta tidsrelaterade egenskaper i tillståndsövergångsmodeller. Huvudproblemet med modellkontroll är problemet med tillståndsexplosion, där antalet tillstånd i modellen kan öka exponentiellt och göra verifieringen ogenomförbar. Tidigare arbete har försökt mildra problemet med tillståndsexplosion genom att representera kodblock som Hoare-logiska kontrakt i en abstrakt tillståndsövergångsmodell med hjälp av tidslogiken TLA. Detta uppnås genom att behandla blocket som atomiskt. För att säkerställa att den abstrakta tillståndsövergångsmodellen är trogen med avseende på de tidsrelaterade egenskaper du vill verifiera kan endast vissa kodblock betraktas som atomiska. Denna avhandling syftar till att besvara hur atomiska kodblock kan identifieras automatiskt och utvärdera deras potential för att minska tillståndsutrymmet under modellkontroll. Vi ger en teoretisk grund för vad det innebär för ett kodblock att betraktas som atomiskt inom TLA. Dessutom introducerar vi en egenskap som karaktäriserar dessa atomiska kodblock och presenterar en algoritm för att identifiera dem för sekventiella program skrivna i en delmängd av C. Experimentella resultat visar att identifieringen av atomiska kodblock med hjälp av vår algoritm kan användas för att betydligt minska tillståndsutrymmet under modellkontroll, med en genomsnittlig reduktionsfaktor på 62. Potentialen för denna verifieringsmetod är lovande, men ytterligare fallstudier krävs för att bättre förstå omfattningen av denna reduktion över olika typer av program och egenskaper.