Scalable validation of binary lifters

Dasgupta, Sandeep

Permalink

https://hdl.handle.net/2142/107968 Copy

Description

Title

Scalable validation of binary lifters

Author(s)

Dasgupta, Sandeep

Issue Date

2020-05-04

Director of Research (if dissertation) or Advisor (if thesis)

Adve, Vikram Sadanand

Doctoral Committee Chair(s)

Adve, Vikram Sadanand

Committee Member(s)

• Rosu, Grigore
• Xie, Tao
• Sekar, R
• Reid, Alastair

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Date of Ingest

2020-08-26T21:54:48Z

Keyword(s)

• x86-64
• Translation Validation
• Formal Semantics
• LLVM
• Compiler Optimizations
• ISA specification

Abstract

The ability to directly reason about binary machine code is desirable, not only because it allows analyzing binaries even when the source code is not available (e.g., legacy code, closed-source software, or malware), but also avoids the need to trust the correctness of compilers. Binary analysis is generally performed by existing decompiler projects by (1) converting raw bytes from the binary into a stream of assembly instructions through disassembly, (2) translating machine code to an intermediate representation (IR) using a binary lifter, and (3) performing various analysis and transformations on the IR pertaining to the specific goals of the decompiler. Many binary analysis frameworks published in academia or as open-source code, use such a lifter as the first step in their pipeline. Validating the correctness of binary lifters is pivotal to gain trust in binary analysis, especially when used in scenarios where correctness is essential. Unfortunately, existing approaches focus on validating the correctness of lifting a single instruction and do not scale to full programs. I believe an effort in the direction would enable both the developers of binary translators, to validate their implementation, and the clients of those translators, to gain trust in their analysis results. The overall goal of my work is to develop formal and informal techniques to achieve high confidence in the correctness of binary lifting by leveraging the semantics of the languages involved (e.g., Intel’s x86-64 and LLVM IR). Towards that goal, I made two broad contributions. First, I defined the most complete and thoroughly tested formal semantics of x86-64 to date. The semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of the x86-64 Haswell instruction set architecture. The formal specification covers 3155 instruction variants, corresponding to 774 mnemonics. The semantics is fully executable and has been tested against the GCC C-torture test suite. Moreover, each instruction is individually tested against more than 7,000 instruction-level test cases. This extensive testing paid off, revealing bugs in both the x86-64 reference manual and other existing semantics, which are all acknowledged, and some are fixed. Also, I illustrated potential applications of the semantics in different formal analyses, and discuss how it can be useful for processor verification. Second, I show that formal translation validation of single instructions for a complex ISA like x86-64 is not only practical but can be used as a building block for scalable full-program validation. My work is the first to do translation validation of single instructions on an architecture as extensive as x86-64, uses the most precise formal semantics available, and has the widest coverage in terms of the number of instructions tested for correctness. Next, we develop a novel technique that uses validated instructions to enable program-level validation, without resorting to performance-heavy semantic equivalence checking. Specifically, I compose the validated IR sequences using a tool we develop called Compositional Lifter to create a reference standard. The semantic equivalence check between the reference and the lifter output is then reduced to a graph-isomorphism check through the use of semantic preserving transformations. The translation validation of instructions in isolation revealed 29 new bugs in McSema – a mature open-source lifter from x86-64 to LLVM IR. Towards the validation of full programs, our approach was able to prove the translational correctness of 2254/2348 functions taken from LLVM’s single-source benchmark test-suite.

Graduation Semester

2020-05

Type of Resource

Thesis

Permalink

http://hdl.handle.net/2142/107968

Copyright and License Information

Copyright 2020 by Sandeep Dasgupta. All rights reserved.

Owning Collections