VADD: Verified Debloating and Delayering

The Verified Debloating and Delayering project aims to build a toolset for application debloating and delayering that produces optimized binaries with reduced attack surfaces from inputs given as existing binaries or source-compiled LLVM bytecode. The project is funded by the Office of Naval Research (ONR).

The VADD tools can be run without developer cooperation after development has completed. The solution integrates formal verification techniques to provide assurance that the optimized program preserves the semantics of the input program.

Binary analysis and modification

VADD supports both source language programs compiled from LLVM and fully compiled x86 binaries. Support for machine code allows applications to be specialized by end users at deployment time.

Our debloating and delayering techniques go beyond traditional compiler optimizations by using additional information about the software configuration, runtime environment, and target platform. This information allows our tools to identify what specific components and functions are needed by an application, specialize functions and data to their identified uses, and remove dead code. Specialized applications only then run on the specific platform, so it should be deferred until that information is known.

Formal assurance

In addition to research in debloating and delayering, our team is addressing the verification and validation challenge of ensuring that transformations do not unintentionally change program behavior. Binary analysis relies on a mix of formal analysis and empirical observations about programming conventions, and our experience suggest that it is very difficult to get right. Our project aims to provide evidence-based formal assurance that the results are correct.

More specifically, we aim to construct an assurance framework capable of providing evidence-based assurance of a complex binary analysis and transformation framework. This verification capability is intended to make sure that binary transformations do not break intended functionality. Our primary performance metrics are: (1) the degree to which the analysis results align with the compiler information generated on binaries that we have source access; and (2) the percentage of the discovered code that we can successfully verify.

In the second half of the program, we will further work on verifying the completeness of our verification capabilities, and this will lead to a third metric, namely the extent to which our translation verifier can itself be shown to cover all the required correctness properties.​

Team and foundation

The VADD team is led by Galois and includes SRI International, Stanford and the University of Iowa. Our team includes experts familiar with all aspects of the problem, and efforts build upon an existing tool foundation that serves as a starting point for our research and transition objectives.

Our efforts will focus on building new innovative work that extends these tools to better deliver on ONR’s cybersecurity program benefits to production applications.

The project depicted is sponsored by the Office of Naval Research under Contract No. N68335-17-C-0558. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Office of Naval Research.