This paper presents data race detection using dynamic symbolic execution and hybrid lockset / happens-before analysis. Symbolic execution is used to explore the execution tree of multi-threaded software for FIFO scheduling on a single CPU core. Compared to exploring the joint scheduling and execution tree, the combinatorial explosion is drastically reduced. An SMT solver is used to control a debugger's machine interface for adaptive dynamic instrumentation to drive program execution into desired paths. Data races are detected in concrete execution with available static binary instrumentation using hybrid analysis. State interpolation using unsatisfiable cores is employed for path pruning, to avoid exploration of paths that do not contribute to increasing branch coverage. An implementation in Eclipse CDT is described and evaluated with data race test cases from the Juliet C/C++ test suite for program analyzers.

We present a new algorithm for the detection of infinite loop bugs in software. Source code is not needed. The algorithm is based on autocorrelation of a program execution's branch target address sequence. We describe the implementation of the algorithm in a dynamic binary instrumentation tool, the result is lightweight enough to be applied continuously at runtime. Functionality of the tool is evaluated with infinite loop bug test cases from the Juliet test suite for program analyzers. Applicability of the algorithm to production software is demonstrated by using the tool to detect previously known infinite loop bugs in cgit, Avahi and PHP.

Software vulnerabilities may be exploited for intruding into a system by an attacker. One approach to mitigation is to automatically analyze software source code in order to find and remove software bugs before release. A method for contextsensitive static bug detection is symbolic execution. This article presents an SMT-constrained static symbolic execution engine with sound path merging. The engine is used by checkers for memory access violation, infinite loops, and atomicity violations. Context information provided by the engine is shared by the different checkers. Further checkers can easily be connected. The engine integrates as plug-in extension into Eclipse CDT and uses CDT’s parser, AST visitor and CFG builder, as well as Eclipse’s GUI and marker framework for bug reporting. The presented approach is evaluated with test cases from the Juliet test suite for C/C++. The evaluation shows a significant speed-up by path merging already for the small Juliet programs. The speed-up depends on the number of decision nodes with more than one satisfiable branch and increases for larger programs. Keywords–Static analysis; Symbolic execution.

Information flow vulnerabilities in UML state charts and C code are detrimental as they can cause data leakages or unexpected program behavior. Detecting such vulnerabilities with static code analysis techniques is challenging because code is usually not available during the software design phase and previous knowledge about what should be annotated and tracked is needed. In this paper we propose textual annotations used to introduce information flow constraints in UML state charts and code which are afterwards automatically loaded by information flow checkers that check if imposed constraints hold or not. We evaluated our approach on 6 open source test cases available in the National Institute of Standards and Technology (NIST) Juliet test suite for C/C++. Our results show that our approach is effective and can be further applied to other types of UML models and programming languages as well, in order to detect different types of vulnerabilities.

Integer overflow errors in C programs are difficult to detect since the C language specification rules which govern how one can cast or promote integer types are not accompanied by any unambiguous set of formal rules. Thus, making it difficult for the programmer to understand and use the rules correctly causing vulnerabilities or costly errors. Although there are many static and dynamic tools used for integer overflow detection, the tools lack the capacity of efficiently filtering out false positives and false negatives. Better tools are needed to be constructed which are more precise in regard to bug detection and filtering out false positives. In this paper, we present an integer overflow checker which is based on precise modeling of C language semantics and symbolic function models. We developed our checker as an Eclipse plug-in and tested it on the open source C/C++ test case CWE-190 contained in the National Institute of Standards and Technology (NIST) Juliet test suite for C/C++. We ran our checker systematically on 2592 programs having in total 340 KLOC with a true positive rate of 95.49% for the contained C programs and with no false positives. We think our approach is effective to be applied in future to C++ programs as well, in order to detect other kinds of vulnerabilities related to integers.

Finding software bugs before deployment is essential to achieve software safety and security. The achievable code coverage and input coverage with manual test suite development at reasonable cost is limited. Therefore, complementary automated methods for bug detection are of interest. This paper describes automated context-sensitive detection of software bugs with dynamic symbolic execution. The program under test is executed in a debugger, and program execution is automatically driven into all program paths that are satisfiable with any program input. Program input and dependent data are treated as symbolic variables. Dynamic analysis and consistent partial static analysis are combined to automatically detect both inputdependent and input-independent bugs. The implementation is a plug-in extension of the Eclipse C/C++ development tools. It uses Eclipse’s code analysis framework, its debugger services framework and a Satisfiability Modulo Theories automated theorem prover. The resulting dynamic symbolic execution engine allows for consistent partially concrete program execution. Compared to static symbolic execution, it transfers as much work as possible to concrete execution in a debugger, without losing bug detection accuracy. The engine is evaluated in terms of bug detection accuracy and runtime on buffer overflow test cases from the Juliet test suite for program analyzers. Keywords–Testing; Program analysis; Symbolic execution.

This paper presents an approach to retargetable SMT-constrained symbolic execution of machine code. The retargetability is based on an existing open-source processor architecture description language which has been used for processor design and automatic generation of toolchains for dynamic program analysis. The benefit of the presented approach is that with a given architecture description, no manual writing of an instruction set grammar or of a translation of instruction semantics into logics is necessary. The proposed tool architecture relies on language reflection, code generation and dynamic loading to retarget symbolic execution to different machine code syntax. Instruction semantics is translated into SMT bit-vector logic equations by symbolically interpreting the architecture description language. The approach is implemented as plug-in extension to the Eclipse IDE and evaluated by automatically detecting integer overflows in binaries for the ARMv5 and SPARCv8 architectures.

In many C programs, debugging requires significant effort and can consume a lot of time. Even if the bug's cause is known, detecting a bug in such programs and generating a bug fix patch manually is a tedious task. In this paper, we present a novel approach used to generate bug fixes for buffer overflow automatically using static execution, code patch patterns, quick fix locations, user input saturation and Satisfiability Modulo Theories (SMT). The generated patches are syntactically correct, can be semi-automatically inserted into code and do not need additional human refinement. We evaluated our approach on 58C open source programs contained in the Juliet test suite and measured an overhead of 0.59% with respect to the bug detection time. We think that our approach is generalizable and can be applied with other bug checkers that we developed.

We present an algorithm for automated detection of infinite loop bugs in programs. It relies on a Satisfiability Modulo Theories (SMT) solver backend and can be run conveniently with SMT-constrained symbolic execution. The algorithm detects infinite loop bugs for single-path, multi-path and nested loops. We prove soundness of the algorithm, i.e. There are no false positive detections of infinite loops. Part of the algorithm is a fixed-point based termination check for 'simple' loops, whose soundness is a consequence of Brouwer's fixed-point theorem. The algorithm further yields no false negative detections for context-sensitive detection of periodic loop orbits with sum of prefix iterations and periodicity of up to the analysis loop unroll depth (bounded completeness), if the SMT solver answers the fixed-point satisfiability query in time. We describe an example implementation as plug-in extension of Eclipse CDT. The implementation is validated with the infinite loop test cases from the Juliet test suite and benchmarks are provided.

This paper presents a combination of symbolic execution and partial order reduction to achieve path-sensitive race detection. The presented approach limits the complexity of symbolic execution of multi-threaded code by applying it with a fixed scheduling algorithm only. Alternative thread interleavings are generated from fixed-scheduling ones with ample set partial order reduction on an abstraction level of thread interactions. Races are detected on the abstraction level. The proposed algorithm is implemented as plug-in extension of Eclipse CDT and evaluated by running it on the race condition test cases from the Juliet suite.

Software vulnerabilities are a major security threat and can often be exploited by an attacker to intrude into systems. One approach to mitigation is to automatically analyze software source code in order to find and remove software bugs before release. A method for context-sensitive static bug detection is symbolic execution. If applied with approximate path coverage, it faces the state explosion problem. The number of paths in the program execution tree grows exponentially with the number of decision nodes in the program for which both branches are satisfiable. In combination with the standard approach using the worklist algorithm with state cloning, this also leads to exponential memory consumption during analysis. This paper considers a source-level symbolic execution engine which uses backtracking of symbolic states instead of state cloning, and extends it with a sound method for merging redundant program paths, based on live variable analysis. An implementation as plugin extension of the Eclipse C/C++ development tools (CDT) is described. The resulting analysis speedup through path merging is evaluated on the buffer overflow test cases from the Juliet test suite for static analyzers on which the original engine had been evaluated. Keywords–Static analysis; Symbolic execution.

Most implementations of public key cryptography employ exponentiation algorithms. Side-channel attacks on secret exponents are typically bound to the leakage of single executions due to cryptographic protocols or side-channel countermeasures such as blinding. We propose for the first time, to use a well-established class of algorithms, i.e. unsupervised cluster classification algorithms such as the k-means algorithm to attack cryptographic exponentiations and recover secret exponents without any prior profiling, manual tuning or leakage models. Not requiring profiling is of significant advantage to attackers, as are well-established algorithms. The proposed non-profiled single-execution attack is able to exploit any available single-execution leakage and provides a straight-forward option to combine simultaneous measurements to increase the available leakage. We present empirical results from attacking an FPGA-based elliptic curve scalar multiplication using the k-means clustering algorithm and successfully exploit location-based leakage from high-resolution electromagnetic field measurements to achieve a low remaining brute-force complexity of the secret exponent. A simulated multi-channel measurement even enables an error-free recovery of the exponent.

Static analysis tools used for detecting information exposure bugs can help software engineers detecting bugs without introducing run-time overhead. Such tools can make the detection of information-flow bugs faster and cheaper without having to provide user input in order to trigger the bug detection. In this paper we present a bug-detection tool for detecting information exposure bugs in C/C++ programs. Our tool is context-sensitive and uses static code analysis for bug detection. We developed our bug finding tool as a Eclipse plug-in in order to easily integrate it in software development work flows. The bug reports provide user friendly visualizations that can be easily traced back to the location where the bug was detected. We discuss one static analysis approach for detecting information exposure bugs and relate briefly the usability of our bug testing tool to empirical research. We conducted an empirical evaluation based on 90 test programs which were selected from the Juliet test suite for C/C++ code. We reached a true-positive coverage of 94.4% in 121 seconds for 90 test programs having a total of 12589 source code lines.

This paper presents a symbolic execution plug-in extension for Eclipse CDT/Codan, which serves to reason about satisfiable paths of C programs. Programs are translated into the SMT-LIB sublogic of arrays, uninterpreted functions and nonlinear integer and real arithmetic (AUFNIRA), and path satisfiability is automatically examined with an SMT solver. The presented plug-in can serve as a basis for path-sensitive static bug detection with bounded or unrestricted context, where the presence of bugs is decided with the solver. An interface provides notifications and context information for checker classes. With a buffer bound checker the symbolic execution plug-in is shown capable of accurately detecting bugs with currently 36 of the 39 C flow variants of the NSA's Juliet test suite for static analyzers.

This paper presents a parallel symbolic execution engine as a plug-in extension to Eclipse CDT/Codan. It uses the CDT parser and the control flow graph builder from CDT’s code analysis framework (Codan). Path satisfiability and bug conditions are checked with an SMT solver in the logic of arrays, uninterpreted functions and nonlinear integer and real arithmetic (AUFNIRA). Each worker of the parallel engine keeps the symbolic program states along its current program path in memory, to allow for quick backtracking. Dynamic redistribution of work between workers is enabled by splitting a worker’s partition of the execution tree at the partition’s top decision node, where a partition is defined by the start path leading to its root control flow decision node. The runtime behaviour of the parallel symbolic execution engine is evaluated by running it on buffer overflow test programs from the NSA’s Juliet test suite for static analyzers. Both the speedup of backtracking the symbolic program state over a previous single-threaded implementation with path replay and the speedup with an increasing number of workers are investigated.

This paper presents an implementation of trusted boot for embedded systems. While in PCs the trusted computing hardware functionality is spread over CPU, memory controller hub (MCH), IO controller hub (ICH) and Trusted Platform Module (TPM), for embedded systems it is desirable to integrate the whole functionality in one system on chip. Our implementation is a two-processor design with LEON3 open source soft cores (SPARC V8 instruction set), coupled over an AHB interface. One of the processors acts as application processor, the other one as `secure' coprocessor. The application processor is synthesized with a boot ROM as static root of trust for measurement. The `secure' coprocessor runs TPM frmware and enables the application processor to boot and run different software while sealing corresponding keys and other secrets to the respective software identity (computed as hash value). We evaluate the design in a Virtex5 FPGA with respect to different measures like resource consumption, code sizes and start times. The `trusted boot' functionality is realised with a boot time increase of around 25% for a Linux system.

We present a new architecture for a secure smart metering system. Our architecture is based on a special purpose hardware security module that encapsulates all security critical operations and provides the main functionality of the system in an active role. This new approach enables secure meter data handling within the smart grid. As a result, our architecture preserves the privacy of sensitive consumer data and the integrity of meter data. Additionally, our proposed solution enhances the security of components critical to the operation of the power grid.

This paper presents an approach for side channel cryptanalysis with iterative approximate Bayesian inference, based on sequential decoding methods. Reliability information about subkey hypotheses is generated in the form of likelihoods, and sets of subkey hypothesis likelihoods are optimally combined into key bit log likelihood ratios. The redundancy of expanded keys in multi-round cryptographic schemes is exploited to correct round key estimation errors. This is achieved by sequential decoding, where subkey candidates are sorted by a probabilistic path metric and iteratively extended. The M-algorithm is presented as a concrete implementation example with deterministic run-time behaviour. The resulting algorithm contains previous hard decision differential analysis as special case for single-round analysis and M=1, and is strictly more accurate otherwise. The trade-off between estimation accuracy and complexity is scalable by parameter choice. The proposed algorithm is simulatively shown in an example scenario to reduce the number of required side channel traces compared to standard differential analysis by a factor of two when run with reasonable complexity, for the whole investigated signal-to-noise ratio range.