Establishing a refinement relation between binaries and abstract code
| Autor: | Joshua A. Bockenek, Binoy Ravindran, Abhijith Bharadwaj, Freek Verbeek, Ian Roessle |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Model checking
Source code Relation (database) Computer science Programming language media_common.quotation_subject Proof assistant HOL 020207 software engineering 0102 computer and information sciences 02 engineering and technology computer.software_genre Data structure 01 natural sciences Variable (computer science) Control flow 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Formal verification Machine code computer media_common |
| Zdroj: | MEMOCODE |
| DOI: | 10.1145/3359986.3361215 |
| Popis: | This paper presents a method for establishing a refinement relation between a binary and a high-level abstract model. The abstract model is based on standard notions of control flow, such as if-then-else statements, while loops and variable scoping. Moreover, it contains high-level data structures such as lists and records. This makes the abstract model amenable for off-the-shelf verification techniques such as model checking or interactive theorem proving. The refinement relation translates, e.g., sets of memory locations to high-level datatypes, or pointer arithmetic to standard HOL functions such as list operations or record accessors. We show applicability of our approach by verifying functions from a binary containing the Network Security Services framework from Mozilla Firefox, running on the x86-64 architecture. Our methodology is interactive. We show that we are able to verify approximately 1000 lines of x86-64 machine code (corresponding to about 400 lines of source code) in one person month. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|