Workshop Program

Abstract:

Picinæ is an infrastructure for machine-proving properties of raw native coe programs without sources within the Coq program-proof co-development system. This facilitates formal reasoning about binary code that is inexpressible in source languages or for which no source code exists, such as hand-written assembly code or code resulting from binary transformations (e.g., binary hardening or debloating algorithms). Preliminary results validating some highly optimized, low-level subroutines for Intel and ARM architectures using this new framework are presented and discussed.

Abstract:

Finite state machine (FSM) is a type of computation models widely used in various software programs. Extracting implemented FSMs has many important applications in network, software engineering and security. In this paper, we first study how FSMs are implemented in real-world software. We then design a static analysis tool, FSMExtractor, to identify and synthesize implemented FSMs. Evaluation using 160 software programs shows that FSMExtractor can extract FSMs with good coverage and accuracy.

Abstract:

We present inuring, a method of live attacker-guided repair of software vulnerabilities. We illustrate inuring with an implementation in an N-variant system. When an N-variant system detects an attack by diverging it converts a grave vulnerability, such as one that enables remote code execution, into a less serious denial-of-service vulnerability; the attacker can repeatedly cause divergence, which crashes or forces a reset of the system. Inuring is a general technique that uses information gleaned from an attack to repair the underlying vulnerability, thereby mitigating the denial-of-service vulnerability. Our demonstration of inuring leverages a novel technique of secure memory layout in N-variant systems. We use a weak memory protection technique in each variant, but are able to guarantee strong protection and remediation for the n-variant system. We present a case study application of inuring to the Apache web server demonstrating the efficacy and efficiency of the technique.

Abstract:

While coverage-based greybox fuzzing has gained great success in the field of vulnerability detection due to its simplicity and efficiency, it could become less powerful when applied directly to protocol fuzzing due to the unique challenges of protocol fuzzing. In particular, the communication among multiple ends contains more than one packet, which are not necessarily dependent upon each other, i.e., fuzzing single (usually the first) packet can only achieve extremely limited code coverage. In this paper, we study such challenges and demonstrate the limitation of current non-stateful greybox fuzzer. In order to achieve higher code coverage, we design and implement a stateful, yield-drive protocol fuzzer, yFuzz, to explore the code related to different protocol states. yFuzz is a stateful fuzzer (which contains a state switching engine, together with a multi-state forkserver) to consistently and flexibly fuzz different states of an compiler-instrumented protocol program. Our experimental results on OpenSSL show that yFuzz achieves an improvement of 73% more code coverage and 2X unique crashes when comparing against fuzzing the first packet during a protocol handshake.

Abstract:

Optimizing a program for a specific machine or a specific workload is possible with today's compilers, but infrequently used, despite significant performance gains. We implement workload specialization, or Profile-Guided Optimization (PGO), at the binary level. Our system CodeMason runs on x86_64 Linux. It performs static binary rewriting to obtain program profiles, then adjusts function ordering, alignment, and other binary-level details to achieve faster performance (particularly on the given workload). We obtain 1.7% average performance speedup on SPEC CPU 2006, and 11.8% speedup in the best case. These substantial performance improvements suggest that binary-level PGO may be widely useful when compiler-based PGO is impossible because the source code is inaccessible.

Abstract:

Software debloating is an emerging field of study aimed at improving the security and performance of software by removing excess library code and features that are not needed by the end user (called bloat). Software bloat is pervasive, and several debloating techniques have been proposed to address this problem. While these techniques are effective at reducing bloat, they are not practical for the average user, risk creating unsound programs and introducing vulnerabilities, and are not well suited for debloating complex software such as network protocol implementations. In this paper, we propose CARVE, a simple yet effective security-focused debloating technique that overcomes these limitations. CARVE employs static source code annotation to map software features source code, eliminating the need for advanced software analysis during debloating and reducing the overall level of technical sophistication required by the user. CARVE surpasses existing techniques by introducing debloating with replacement, a technique capable of preserving software interoperability and mitigating the risk of creating an unsound program or introducing a vulnerability. We evaluate CARVE in 12 debloating scenarios and demonstrate security and performance improvements that meet or exceed those of existing techniques.

Abstract:

Code bloating in shared code modules has been proven pervasive in recent research. However, each study provides a different approach to measuring bloat in software. In this paper, we propose a system of metrics to effectively quantify bloating in binaries. Using them as pointers, we introduce a static approach to perform debloating for closed source code applications by creating specialized versions of shared libraries depending on how they are used by applications as indicated by our bloat factors. We conduct an extensive study and calculate bloat factors for over 3000 Linux applications using 896 shared libraries and provide directions for both debloating as well as future library development process. We evaluate our debloating technique on large programs and achieve a maximum code reduction of 25%.