Binary-level pointer analysis can be of use in symbolic execution, testing, verification, and decompilation of software binaries. In various such contexts, it is crucial that the result is trustworthy, i.e., it can be formally established that the pointer designations are overapproximative. This paper presents an approach to formally proven correct binary-level pointer analysis. A salient property of our approach is that it first generically considers what proof obligations a generic abstract domain for pointer analysis must satisfy. This allows easy instantiation of different domains, varying in precision, while preserving the correctness of the analysis. In the trade-off between scalability and precision, such customization allows “meaningful” precision (sufficiently precise to ensure basic sanity properties, such as that relevant parts of the stack frame are not overwritten during function execution) while also allowing coarse analysis when pointer computations have become too obfuscated during compilation for sound and accurate bounds analysis. We experiment with three different abstract domains with high, medium, and low precision. Evaluation shows that our approach is able to derive designations for memory writes soundly in COTS binaries, in a context-sensitive interprocedural fashion.

This paper studies an extension of O’Hearn’s incorrectness logic (IL) that allows backwards reasoning. IL in its current form does not generically permit backwards reasoning. We show t at this can be mitigated by extending IL with underspecification. The resulting logic combines underspecification (the result, or postcondition, only needs to formulate constraints over relevant variables) with underapproximation (it allows to focus on fewer than all the paths). We prove soundness of the proof system, as well as completeness for a defined subset of presumptions. We discuss proof strategies that allow one to derive a presumption from a given result. Notably, we show that the existing concept of loop summaries- closed-form symbolic representations that summarize the effects of executing an entire loop at once- is highly useful. The logic, the proof system and all theorems have been formalized in the Isabelle/HOL theorem prover.

Analysis of binary software plays a critical role in software security. Reverse engineers analyze binaries to discover vulnerabilities, patch legacy software, and detect malware. Most of the reverse engineering tools have been developed from a practical point of view, and do not provide any guarantees with their results. Recently, formally verified reverse engineering and decompilation have gained traction. These formal tools are for the most part proof-of-concept systems not yet suitable for real-world reverse-engineering tasks. In this poster, we explore the idea of formalizing part of an existing decompilation tool instead. We focus on the lifting from assembly to the IR P-Code in one of the most popular decompilers, Ghidra. This step occurs immediately after disassembly. We are developing a proof system inside the Isabelle theorem prover, to automatically prove semantical equivalence between the assembly and P-Code instructions. We leverage machine-learned x86-64 semantics, to stay as close as possible to actual CPU behavior. This approach has uncovered several shortcomings in Ghidra's P-Code and the lifting it performs. By using a theorem prover, we obtain guarantees that our system of formal semantics and lifting is internally consistent. This work brings the powerful guarantees that formal methods provide in reverse engineering research to the real world.

We present an approach to lift position-independent x86-64 binaries to symbolized NASM. Symbolization is a decompilation step that enables binary patching: functions can be modified, and instructions can be interspersed. Moreover, it is the first abstraction step in a larger decompilation chain. The produced NASM is recompilable, and we extensively test the recompiled binaries to see if they exhibit the same behavior as the original ones. In addition to testing, the produced NASM is accompanied with a certificate, constructed in such a way that if all theorems in the certificate hold, symbolization has occurred correctly. The original and recompiled binary are lifted again with a third-party decompiler (Ghidra). These representations, as well as the certificate, are loaded into the Isabelle/HOL theorem prover, where proof scripts ensure that correctness can be proven automatically. We have applied symbolization to various stripped binaries from various sources, from various compilers, and ranging over various optimization levels. We show how symbolization enables binary-level patching, by tackling challenges originating from industry.

Even though heavily researched, a full formal model of the x86-64 instruction set is still not available. We present libLISA , a tool for automated discovery and analysis of the ISA of a CPU. This produces the most extensive formal x86-64 model to date, with over 118 000 different instruction groups. The process requires as little human specification as possible: specifically, we do not rely on a human-written (dis)assembler to dictate which instructions are executable on a given CPU, or what their in- and outputs are. The generated model is CPU-specific: behavior that is “undefined” is synthesized for the current machine. Producing models for five different x86-64 machines, we mutually compare them, discover undocumented instructions, and generate instruction sequences that are CPU-specific. Experimental evaluation shows that we enumerate virtually all instructions within scope, that the instructions’ semantics are correct w.r.t. existing work, and that we improve existing work by exposing bugs in their handwritten models.

Lifting binaries to a higher-level representation is an essential step for decompilation, binary verification, patching and security analysis. In this paper, we present the first approach to provably overapproximative x86-64 binary lifting. A stripped binary is verified for certain sanity properties such as return address integrity and calling convention adherence. Establishing these properties allows the binary to be lifted to a representation that contains an overapproximation of all possible execution paths of the binary. The lifted representation contains disassembled instructions, reconstructed control flow, invariants and proof obligations that are sufficient to prove the sanity properties as well as correctness of the lifted representation. We apply this approach to Linux Foundation and Intel’s Xen Hypervisor covering about 400K instructions. This demonstrates our approach is the first approach to provably overapproximative binary lifting scalable to commercial off-the-shelf systems. The lifted representation is exportable to the Isabelle/HOL theorem prover, allowing formal verification of its correctness. If our technique succeeds and the proofs obligations are proven true, then – under the generated assumptions – the lifted representation is correct.

Abstract We present a methodology for generating a characterization of the memory used by an assembly program, as well as a formal proof that the assembly is bounded to the generated memory regions. A formal proof of memory usage is required for compositional reasoning over assembly programs. Moreover, it can be used to prove low-level security properties, such as integrity of the return address of a function. Our verification method is based on interactive theorem proving, but provides automation by generating pre- and postconditions, invariants, control-flow, and assumptions on memory layout. As a case study, three binaries of the Xen hypervisor are disassembled. These binaries are the result of a complex build-chain compiling production code, and contain various complex and nested loops, large and compound data structures, and functions with over 100 basic blocks. The methodology has been successfully applied to 251 functions, covering 12,252 assembly instructions.

This paper presents a methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x86-64 machine model containing small step semantics for 1625 instructions. Second, a decompilation-into-logic methodology supporting both x86-64 assembly and machine code at large scale. This work enables black-box binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safety-critical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machine-learned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floating-point instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code.

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.

In modern many-core architectures, advanced on-chip networks provide the means of communication for the cores. This greatly complicates the design and verification of the cache coherence protocols deployed by those cores. A common approach to deal with this complexity is to decompose the whole system into the protocol and the network. This decomposition is, however, not always possible. For example, unexpected deadlocks can emerge when a deadlock-free protocol and a deadlock-free network are combined. This paper proposes a compositional methodology: prove properties over a network, prove properties over a protocol, and infer properties over the system as a whole. Our methodology is based on theorems that show that such decomposition is possible by having sufficiently large local buffers at the cores. We apply this methodology to verify several protocols such as MI, MSI, MESI and MEUSI running on top of advanced interconnects with adaptive routing.

Latency is a major issue in the design and validation of a Network-on-Chip (NoC). Various techniques for establishing latency bounds exist. Formal and mathematical methods, such as network calculus, can be used to analyze an NoC model. Simulation-based methods can be used to estimate latency bounds by exploring reachable states. Both have their advantages and disadvantages. This paper presents an approach that finds a middle ground between these two worlds. Our approach is based on simulation of high-level formal models. In contrast to traditional formal methods for worst-case latency, we do not require error-prone manual computation or the absence of cycles. In contrast to traditional simulation-based methods, we leverage the high level of abstraction to explore up to billions of states within a couple of hours. We apply our approach on an 8 core case study where a simple cache protocol runs on top of a ring-based Spidergon architecture. We show that deadlocks or starvations are easily found, and that for live networks a worst-case bound estimation can be produced within reasonable time.

Cache coherence plays a major role in manycore systems. The verification of deadlocks is a challenge in particular, because deadlock freedom is an emerging property. Formal methods often decouple verification of the protocol from verification of the communication interconnect. Modern communication fabrics, however, become more advanced and include a network topology, routing, arbitration, synchronization, and more. In this paper, an integrated approach is proposed that allows cross-layer verification of both the cache coherence protocol and the communication fabric all at once. An automated methodology for deriving cross-layer invariants is proposed. These invariants relate the state of the application-layer protocols to en route packets in the communication fabric. Using the invariants, we derive formal proofs of deadlock-freedom for two case studies: a directory-based MI protocol in a 2D mesh, and a ring-based snoopy protocol in a 2D torus. Additionally, we show that our methodology can be used to derive the smallest possible queue sizes that ensure absence of deadlocks. Our methodology is generally applicable and shows promising scalability.

In the multi-core era, on-chip communication networks are key to system correctness and performance. To deal with their growing complexity, micro-architectural models capture the intent of architects and provide means for formal analysis. However, the analysis of such micro-architectural models is restricted to non-scalable and/or very specific approaches. We present a novel scalable approach to support the symbolic channel type inference of large micro-architectural models described in the xMAS language proposed by Intel. We define an algorithm that computes all possible messages that can occur in a communication channel, treating their payload symbolically. These results can be used for further analysis such as verifying absence of misrouting, deriving inductive invariants and deadlock detection. We illustrate our approach on a Spidergon network developed at STMicroelectronics.

Deadlock freedom is a key challenge in the design of communication networks. Wormhole switching is a popular switching technique, which is also prone to deadlocks. Deadlock analysis of routing functions is a manual and complex task. We propose an algorithm that automatically proves routing functions deadlock-free or outputs a minimal counter-example explaining the source of the deadlock. Our algorithm is the first to automatically check a necessary and sufficient condition for deadlock-free routing. We illustrate its efficiency in a complex adaptive routing function for torus topologies. Results are encouraging. Deciding deadlock freedom is co-NP-Complete for wormhole networks. Nevertheless, our tool proves a 13 × 13 torus deadlock-free within seconds. Finding minimal deadlocks is more difficult. Our tool needs four minutes to find a minimal deadlock in a 11 × 11 torus while it needs nine hours for a 12 × 12 network.

This article presents a formal specification and validation environment to prove safety and liveness properties of parametric -- unbounded -- NoCs architectures described at a high-level of abstraction. The environment improves the GeNoC approach with two new theorems, proving evacuation and starvation freedom. The application of the validation methodology is illustrated on a HERMES NoC with adaptive west-first routing and wormhole switching. This case study illustrates the strong compositional aspect of the GeNoC environment. The complete specification of this HERMES instance, together with the proof that the specification is deadlock-free, starvation free, and all messages eventually leave the network at their correct destination, could be achieved in about a week. Approximately 86% of this proof is automatically derived from the GeNoC model.

Cache coherency is one of the major issues in multicore systems. Formal methods, in particular model-checking, have been successful at verifying high-level protocols, but, to the best of our knowledge, the verification of cache coherency at the architectural level is still an open issue. All existing verification efforts assume a reliable interconnect, that is, messages eventually reach their destination. We discuss the challenge of discharging this assumption at the architectural level where implementation details of the interconnect are mixed with a cache coherency protocol. Our automatic approach is based on a well-defined set of primitives to express architectural models, a generic model of communication fabrics expressed in an automated theorem proving system, and a dedicated algorithm for deadlock and livelock detection. We argue that reliability depends on the interaction between the interconnect and the cache coherency protocol. They must be verified altogether as their combination creates intricate message dependencies. We sketch our verification approach and apply it to a simple write-invalidate protocol on the Spidergon network-on-chip from STMicroelectronics. Our approach is promising. For this simple protocol, networks with tens of agents and hundreds of components can be analyzed within seconds.

Wormhole switching is a switching technique nowadays commonly used in networks-on-chips (NoCs). It is efficient but prone to deadlock. The design of a deadlock-free adaptive routing function constitutes an important challenge. We present a novel algorithm for the automatic verification that a routing function is deadlock-free in wormhole networks. A sufficient condition for deadlock-free routing and an associated algorithm are defined. The algorithm is proven complete for the condition. The condition, the algorithm, and the correctness theorem have been formalized and checked in the logic of the ACL2 interactive theorem proving system. The algorithm has a time complexity in O(N3), where N denotes the number of nodes in the network. This outperforms the previous solution of Taktak et al. by one degree. Experimental results confirm the high efficiency of our algorithm. This paper presents a formally proven correct algorithm that detects deadlocks in a 2D-mesh with about 4000 nodes and 15000 channels within seconds.

Deadlocks are an important issue in the design of interconnection networks. A successful approach is to restrict the routing function such that it satisfies a necessary and sufficient condition for deadlock-free routing. Typically, such a condition states that some (extended) dependency graph must be a cyclic. Defining and proving such a condition is complex. Proving that a routing function satisfies a condition can be complex as well. In this paper we present the first algorithm that automatically proves routing functions deadlock-free for store-and-forward networks. The time complexity of our algorithm is linear in the size of the resource dependency graph. The algorithm checks a variation of Duato's condition for adaptive routing. The condition and the algorithm have been formalized in the logic of the ACL2 interactive theorem prover. The correctness of our algorithm w.r.t. the condition is formally checked using ACL2.

The purpose of this comment is to show that Duato's condition for deadlock freedom is only sufficient and not necessary. We propose a fix to keep the condition necessary. The issue is subtle but essential: in a wormhole network worms necessarily do not intersect.

Wormhole switching is a popular switching technique in interconnection networks. This technique is also prone to deadlocks. Adaptive routing algorithms provide alternative paths that can be used to escape congested areas and prevent some deadlocks to occur. If not designed carefully, these new paths may as well introduce deadlocks. A successful solution to deadlock prevention is to constrain the routing function such that it does not introduce any deadlock. Many necessary and sufficient conditions for deadlock-free routing have been proposed. The definition and the proof of these conditions are complex and error-prone. These conditions are often counterintuitive and difficult to understand. Moreover, they are not static, as they all require the analysis of configurations, i.e., the network state. The contribution of this paper is twofold. We present the first static necessary and sufficient condition for deadlock-free routing in wormhole networks. Our condition is much simpler and requires less assumptions than all previous ones. It is formally proven correct using an automated proof assistant. In particular, our condition applies to incoherent routing functions which was considered an open problem. Second, we prove the deadlock decision problem co-NP-complete for wormhole networks.

Networks-on-chips (NoC) are emerging as a promising interconnect solution for efficient Multi-Processors Systems-on-Chips. We propose a methodology that supports the specification of parametric NoCs. We provide sufficient constraints that ensure deadlock-free routing, functional correctness, and liveness of the design. To illustrate our method, we discharge these constraints for a parametric NoC inspired by the HERMES architecture.