The security of a software program critically depends on the prevention of vulnerabilities in the source code; however, conventional computer programs lack the ability to identify vulnerable code in another program. Our research was aimed at developing a technique capable of generating substitution code for the detection of buffer overflow vulnerability in C/C++ programs. The technique automatically verifies and sanitizes code instrumentation by comparing the result of each candidate variable with that expected from the input data. Our results showed that statements containing buffer overflow vulnerabilities could be detected and prevented by using a substitution variable and by sanitizing code vulnerabilities based on the size of the variables. Thus, faults can be detected prior to execution of the statement, preventing malicious access. Our approach is particularly useful for enhancing software security monitoring, and for designing retrofitting techniques in applications.

Return-oriented programming (ROP) attacks, which have been increasing in number recently, are an exploitation technique that can bypass non-executable page protection methods by using codes that exist within benign programs or modules. There have been many studies on defense against ROP attacks, but most of them have high overhead or high time complexity in terms of the detection of gadgets. In this letter, we suggest an ROP defense technique which is fast, space-efficient, and of lower detection time complexity; it uses a compiler-based approach. The most recent ROP defense technique is a compiler-based zero-sum defender suggested by Kim et al., achieving very low overhead. However, it still did not solve the issue of time complexity regarding detection. Our technique performs a specific computation to identify gadgets at the resetting position immediately before and after a return instruction. This method can efficiently identify a series of gadgets performed without calls and defend against them. In our experiment, the performance overhead was 1.62% and the file size overhead was 4.60%; our proposed technique achieved O(1) in terms of time complexity while having almost the same overhead as the zero-sum defender.

Recently, return-oriented programming (ROP) attacks have been rapidly increasing. In this letter, we introduce a fast and space-efficient defense technique, called zero-sum defender, that can respond against general ROP attacks. Our technique generates additional codes, at compile time, just before return instructions to check whether the execution has been abused by ROP attacks. We achieve very low runtime overhead with very small increase in file size. In our experimental results, performance overhead is 1.7%, and file size overhead is 4.5%.

A buffer overflow attack occurs when a program writes data outside the allocated memory in an attempt to invade a system. Approximately forty percent of all software vulnerabilities over the past several years are attributed to buffer overflow. Taint tracking is a novel technique to prevent buffer overflow. Previous studies on taint tracking ran a victim's program on an emulator to dynamically instrument the code for tracking the propagation of taint data in memory and checking whether malicious code is executed. However, the critical problem of this approach is its heavy performance overhead. Analysis of this overhead shows that 60% of the overhead is from the emulator, and the remaining 40% is from dynamic instrumentation and taint information maintenance. This article proposes a new taint-style system called Embedded TaintTracker to eliminate the overhead in the emulator and dynamic instrumentation by compressing a checking mechanism into the operating system (OS) kernel and moving the instrumentation from runtime to compilation time. Results show that the proposed system outperforms the previous work, TaintCheck, by at least 8 times on throughput degradation, and is about 17.5 times faster than TaintCheck when browsing 1 KB web pages.

Many malicious programs we encounter these days are armed with their own custom encoding methods (i.e., they are packed) to deter static binary analysis. Thus, the initial step to deal with unknown (possibly malicious) binary samples obtained from malware collecting systems ordinarily involves the unpacking step. In this paper, we focus on empirical experimental evaluations on a generic unpacking method built on a dynamic binary instrumentation (DBI) framework to figure out the applicability of the DBI-based approach. First, we present yet another method of generic binary unpacking extending a conventional unpacking heuristic. Our architecture includes managing shadow states to measure code exposure according to a simple byte state model. Among available platforms, we built an unpacking implementation on PIN DBI framework. Second, we describe evaluation experiments, conducted on wild malware collections, to discuss workability as well as limitations of our tool. Without the prior knowledge of 6029 samples in the collections, we have identified at around 64% of those were analyzable with our DBI-based generic unpacking tool which is configured to operate in fully automatic batch processing. Purging corrupted and unworkable samples in native systems, it was 72%.

Although software-attack detection via dynamic taint analysis (DTA) supports high coverage of program execution, it prohibitively degrades the performance of the monitored program. This letter explores the possibility of collaborative dynamic taint analysis among members of an application community (AC): instead of full monitoring for every request at every instance of the AC, each member uses DTA for some fraction of the incoming requests, thereby loosening the burden of heavyweight monitoring. Our experimental results using a test AC based on the Apache web server show that speedy detection of worm outbreaks is feasible with application communities of medium size (i.e., 250-500).

Many Internet services and protocols should guarantee anonymity; for example, an electronic voting system should guarantee to prevent the disclosure of who voted for which candidate. To prove trace anonymity, which is an extension of the formulation of anonymity by Schneider and Sidiropoulos, this paper presents an inductive method based on backward anonymous simulations. We show that the existence of an image-finite backward anonymous simulation implies trace anonymity. We also demonstrate the anonymity verification of an e-voting protocol (the FOO protocol) with our backward anonymous simulation technique. When proving the trace anonymity, this paper employs a computer-assisted verification tool based on a theorem prover.

The use of a formal method is a promising approach to developing reliable computer programs. This paper presents a formal method for anonymity, which is an important security property of communication protocols with regard to a user's identity. When verifying the anonymity of security protocols, we need to consider the presence of adversaries. To formalize stronger adversaries, we introduce an adversary model for simulation-based anonymity proof. This paper also demonstrates the formal verification of a communication protocol. We employ Crowds, which is an implementation of an anonymous router, and verify its anonymity. After describing Crowds in a formal specification language, we prove its anonymity with a theorem prover.

Many computer systems are designed to make it easy for end-users to install and update software. An undesirable side effect, from the perspective of many software producers, is that hostile end-users may analyze or tamper with the software being installed or updated. This paper proposes a way to avoid the side effect without affecting the ease of installation and updating. We construct a computer system M with the following properties: 1) the end-user may install a program P in any conveniently accessible area of M; 2) the program P contains encoded instructions whose semantics are obscure and difficult to understand; and 3) an internal interpreter W, embedded in a non-accessible area of M, interprets the obfuscated instructions without revealing their semantics. Our W is a finite state machine (FSM) which gives context-dependent semantics and operand syntax to the encoded instructions in P; thus, attempts to statically analyze the relation between instructions and their semantics will not succeed. We present a systematic method for constructing a P whose instruction stream is always interpreted correctly regardless of its input, even though changes in input will (in general) affect the execution sequence of instructions in P. Our framework is easily applied to conventional computer systems by adding a FSM unit to a virtual machine or a reconfigurable processor.