Jinwei Hu

Heiko Mantel

Sebastian Ruhleder
email: sebastian.ruhleder@googlemail.com

Enforcing Usage Constraints on Credentials for Web Applications

For using credential-based access control effectively, recent work identified the need to enforce usage constraints also on credentials. The enforcement of such constraints has not yet been investigated for web applications, although it is relevant when credential-based access control is employed in a web application. This article proposes an approach suitable for enforcing usage constraints on credentials in web applications. More concretely, we present a novel algorithm and an implementation of this algorithm that construct constraint-compliant proofs for credentialbased access control policies. We proved that our solution is correct and showed that it is also efficient through extensive experiments.

Introduction

Many web applications control access to their resources using policies that state which attributes a client must have in order to obtain access. For example, an online svn system in a university might allow a client to view a directory if some employee of the university owns the directory and if the employee nominates the client as a collaborator. One promising approach to enforce a policy like this is credential-based access control (CBAC) [START_REF] Vimercati | Integrating trust management and access control in data-intensive web applications[END_REF].

In CBAC, credentials are used to encode attributes of clients. The representation of credentials may vary, but usually digitally-signed certificates are used as representation. Which credentials a client must provide in order to obtain a particular access is specified by an access control policy. Hence, before granting access, an enforcement mechanism needs to check that the provided credentials legitimate the desired access. This last step is known as proof construction.

Recent work on CBAC identified a need to also restrict the usage of credentials [START_REF] Bauer | Constraining credential usage in logic-based access control[END_REF][START_REF] Hu | Compliance checking for usage-constrained credentials in trust negotiation systems[END_REF], in particular, if CBAC is employed in open systems. In an open, distributed system, a credential might be issued with a particular purpose, but it is hardly possible for a credential issuer to exclude the possibility that the credential might be exploitable in other, unintended ways. The danger is that a credential is used in the construction of proofs that result in authorizations unforeseen by the issuer. Usage constraints on credentials enable credential issuers to better control the use of their credentials. They allow issuers to encode the purpose of a credential, thus, reducing the threat of misuse.

Usage constraints on credentials are obviously relevant for web applications that employ CBAC. However, the enforcement of usage constraints on credentials has not been investigated in this domain yet. Moreover, solutions in other domains cannot be transferred to web applications in a straightforward manner, as web applications pose new challenges to enforcing usage constraints on credentials. For instance, if a web application needs to respond to requests with low latencies, even under high workloads, then a web application developer is likely reluctant to adopt a usage constraint for credentials that causes substantial overhead. This is the challenge that we address in this article.

We present a novel algorithm for constructing proofs (1) that soundly certify compliance with a given CBAC policy and ( 2) that respect all usage constraints of credentials used during proof construction. Moreover, our algorithm is complete in the sense that it is able to generate all proofs that comply with (1) and [START_REF] Bauer | Constraining credential usage in logic-based access control[END_REF]. The feature of generating all constraint-compliant proofs is driven by the need to strategically manage credential disclosure to, for example, minimize the number or sensitivity of credentials sent to an application [START_REF] Lee | Towards an efficient and language-agnostic compliance checker for trust negotiation systems[END_REF][START_REF] Oster | Model checking of qualitative sensitivity preferences to minimize credential disclosure[END_REF]. With all proofs at hand, one could choose a proof that meets a strategy.

In the implementation of our solution, we followed the idea of proof-carrying authorization to web applications [START_REF] Bauer | Access Control for the Web via Proof-carrying Authorization[END_REF]. More concretely, we implemented a browser extension for deploying our proof-construction algorithm. A client adds this extension for requesting resources at a web application. A web application simply checks the validity of a proof received from a client which uses the browser extension. In this way, the application only needs to incorporate a proof-checking functionality.

To sum up, our main technical contribution is a novel algorithm for constructing constraint-compliant proofs. We proved the correctness of our algorithm and demonstrated its effectiveness and efficiency in experiments.

The rest of the article is organized as follows. We present preliminaries and our problem statement in Section 2. In Section 3, we present our algorithm, including the algorithm description and the correctness theorem. We describe our implementation in Section 4, followed by the performance evaluation of our algorithm in Section 5. Finally, we discuss related work and conclude in Section 6.

Preliminaries and Problem Statement

Credential-based access control. We use the policy language RT 0 [START_REF] Li | Distributed credential chain discovery in trust management[END_REF], a rolebased trust management language, to express credentials. RT 0 has four types of credentials:

-Simple membership A.R ← D: principal D is assigned to role A.R. -Simple containment A.R ← B.R 1 : principals assigned to role B.R 1 are also assigned to role A.R. -Linking containment A.R ← A.R 1 .R 2 : principals assigned to role B.R 2 with
B being assigned to role A.R 1 are also assigned to role A.R. -

A.R ← D D in A.R sm D in B.R1 A.R ← B.R1 D in A.R sc B in A.R1 D in B.R2 A.R ← A.R1.R2 D in A.R lc D in B1.R1 • • • D in B k .R k A.R ← B1.R1 ∩ . . . ∩ B k .R k D in A.R ic
Intersection containment A.R ← B 1 .R 1 ∩ . . . ∩ B n .
R n : a principal is assigned to role A.R if the principal is also assigned to all the roles B 1 .R 1 , . . ., and

B n .R n .
The semantics of RT 0 credentials is formalized by the inference rules in Figure 1, where D in A.R denotes the principal D's membership of role A.R. For a credential of the form X ← Y , we say X is the head and Y is the body of the credential. Readers are referred to [START_REF] Li | Distributed credential chain discovery in trust management[END_REF] for more details of RT 0 . In RT 0 , roles are used to model particular accesses to particular resources. For example, one could introduce a role U niv.network, where U niv is a principal and network is a role name, to model access to networks of U niv. In turn, to access a particular resource one needs to have a membership in the role to which this resource corresponds.

Role memberships are granted based on credentials. For example, the credential U niv.network ← Alice grants the membership in U niv.network to Alice. For another example, the credentials in the following set jointly grant to Alice the membership in the role U niv.network. In both cases, one actually derives a proof of the membership using the provided credentials. A proof (p, r, c, s) shows the membership of p in r. Thus, upon seeing the proof, a system deploying credential-based access control allows the access of p to the resource represented by r. We say a proof (p, r, c, s) uses a credential if it is c or it is used by the sub-proofs in s.

U
Usage constraints on credentials. As discussed in [START_REF] Bauer | Constraining credential usage in logic-based access control[END_REF][START_REF] Hu | Compliance checking for usage-constrained credentials in trust negotiation systems[END_REF], credential issuers are in need of specifying constraints on how their credentials are used, in addition to the language support (e.g., RT ). Typical example constraints include delegation depth and final-usage constraints. Following [START_REF] Hu | Compliance checking for usage-constrained credentials in trust negotiation systems[END_REF], we define a constraint as a deterministic finite automaton (DFA) (Q, Σ, δ, q 0 , F ), where Q is a finite set of states, Σ is a finite set of input symbols, δ : Q × Σ → Q is a transition function, q 0 ∈ Q is an initial state, and F ⊆ Q is a set of final states. The input set Σ of a constraint shall be instantiated with the set of roles in the set CS of credentials when constructing proofs based on CS.

To define the semantics of constraints, we let words(P ) be words of a proof P = (p, r, c, s) such that words(P ) = {r} if s = ∅ and, otherwise, words(P ) = {r; w ∈ Σ * | ∃P ∈ s : w ∈ words(P )}. A proof (p, r, c, s) based on CS satisfies a constraint if all words of the proof are accepted by the constraint. Informally, a constraint restricts which roles may appear in a proof and where they may appear in the proof.

q 0 q 1 q 2 U niv.internal Σ Σ\{U niv.internal} Σ Figure 2: An example constraint.
For example, suppose that U niv wants to prevent its credential c1 = U niv.network ← U niv.guest from being used for proving memberships in role U niv.internal, regardless of whichever credentials have been issued or may be issued later. This is a final usage constraint on c1; U niv could specify the DFA in Figure 2 as a constraint and attach the constraint to c1. This constraint excludes any proof of the form (p, U niv.internal, c, s). Receiving words of such a proof, the automaton transits from state q 0 to q 1 with the input U niv.internal; if s = ∅, the automaton stays at state q 1 with input r i for any sub-proofs (p i , r i , c i , s i ) ∈ s. Hence, the automaton could not reach a final state, which means that the proof does not satisfy the constraint. On the other hand, for a proof of the form (p, r, c, s) where r = U niv.internal, its words are accepted by the automaton and thus the proof satisfies the constraint.

In principle, each credential may come along with a constraint specifying its usage. We say a proof is constraint-compliant if it satisfies all constraints that are attached to the credentials used in the proof.

Definition 2 (Problem statement). Given a set CS of credentials, a principal p, and a role r, the problem is to find all constraint-compliant proofs of p in r based on CS.

Algorithm

This section presents our algorithm Sage that solves the problem in Definition 2. We first describe the algorithm and then discuss its correctness.

Overview. The Sage algorithm, as shown in Figure 3, is essentially a depthfirst search algorithm. It makes use of a dependency between c and s in a proof P = (p, r, c, s): The inference rule used to conclude the role membership p in r must take the credential c and all sub-proofs s i ∈ s as its premise; further, the rule must match one of the four inference rules sm, sc, ic, and lc. Consequently, the type of the credential c directly determines what proofs must be present in s for this to be possible. The Sage algorithm utilizes this dependency between c and s to construct proofs recursively: When a role membership p in r shall be proven, (1) select all credentials with r as the head; (2) for every such credential, (2i) identify the role memberships that must be proven in order to satisfy the premise of an appropriate inference rule, and (2ii) then call the Sage algorithm again with the same principal for every identified role membership. If all necessary role memberships can be proven, construct (and later return) a proof with the recursively constructed proofs and the associated, previously selected credential.

Main procedure. The entry point of Sage is the Sage-Prove function: It takes a set of credentials, a role, and a principal as input and returns a set of proofs showing the membership of the principal in the role. Sage consists mainly of two parts: initialization and proof construction.

Initialization. Sage first converts the credentials into nodes. Sage uses nodes, each of which is a container for credentials with the same head role. Sage stores every credential c ∈ CS in exactly one node, i.e. the node associated to its head role. The use of nodes provides a simplified way to access different credentials in the set CS. Sage initializes the constraints as an empty set, as no credential has been used for proofs yet.

Proof construction. Sage calls the Construct-Proofs function to compute the set of proofs. Function Construct-Proofs consists of three stages: preprocessing (Lines 1 -7), sub-proof construction (Lines 8 -19), and post-processing (Line 20). The pre-processing stage checks whether any proofs may be constructed; the sub-proof construction stage proceeds to construct sub-proofs with different types of credentials. The post-processing stage checks additional constraints that proofs should comply with.

Pre-processing. Line 1 extends the role path with the provided role r . Given a proof (p, r, c, s), a role path is a sequence of roles, starting with r and being followed by a role path of a proof in s. Note that a proof may have multiple role paths. This extended role path serves as a trace at which point the algorithm is in relation to the overall structure of the constructed proofs. In lines 2 -4, this extended role path is used to check whether all constraints in the set constraints can still reach a final state from it. If not, any further proofs do not comply with at least one of the constraints. Line 5 checks whether there is any credential available to construct further proofs. If so, the associated node is then assigned to the variable node and the set proofs is initialized as an empty set. The set proofs serves as a container for proofs.

Sub-proof construction. Lines 8 -19 construct sub-proofs for each type of credentials. First, lines 8 -9 traverse all simple member credentials of node and add to the set proofs a proof for each credential r ← p. Lines 10 -19 traverse the set of credentials of node to construct proofs for the three remaining types of credentials (simple, intersection, or linking containment). Depending on the type of credentials, a helper function is invoked (lines 12 -17). Each function returns a collection of sets of sub-proofs that can be used to construct proofs in combination with c. Note that the helper functions also call Construct-Proofs for proof construction. Please see Appendix A for the helper functions. Line 19 combines the returned sets of sub-proofs with credential c to a proof of p's membership in r .

Post-processing. Line 20 (Filter-Valid-Proofs) filters proofs that satisfy all remaining constraints. Recall that the filtering at lines 2 -4 checks constraints of a selected credential; this check does not concern constraints introduced posterior to the selected credential. Filter-Valid-Proofs checks those latter constraints. In combination, these two checks ensure that Sage returns only constraint-compliant proofs.

Algorithm correctness. Given a set of credentials CS, a principal p, and a role r, we let Proofs(C, r, p) be the set of constraint-compliant proofs of p in r. That is, Proofs(C, r, p) contains all the proofs that show the membership of p in r, according to the semantics of RT 0 and constraints. Let Sage-Prove(C, r, p) be the set of proofs returned by the algorithm in Figure 3.

Theorem 1. Given a set of credentials CS, a principal p, and a role r, Sage-Prove(C, r, p) = Proofs(C, r, p).

Proof sketch: We prove two lemmas:

1. Sage-Prove(C, r, p) ⊆ Proofs(C, r, p) (i.e., any proof returned by the algorithm is constraint-compliant), and 2. Sage-Prove(C, r, p) ⊇ Proofs(C, r, p) (i.e., any constraint-compliant proof will be generated by the algorithm).

We first map a proof (p, r, c, s) to a tree where the root is the proof itself and its children are the sub-proofs in the set s. The height of a proof is then defined as the height of this tree. We then prove the two lemmas by induction on the height. The full proof of the theorem is available on the authors' website.

Implementation

To implement the proposed approach for web applications, we first adapt the communication process between a client and a web application. As shown in Figure 4, the communication takes four steps: (1) The client sends a request for a resource to the application. ( 2) Upon receiving a request, the application returns a policy for the client to prove. (3) The client constructs a proof of the policy and sends the proof and the credentials together to the application. (4) The application sends the response to the client. If the proof is checked constraint-compliant, the resource is sent to the client; otherwise not. Among the four steps, step (2) employs the Sage algorithm proposed in Section 3. We implement the algorithm in a browser extension. As such, users at the client need not interact with CBAC when requesting resources. At the web application side, we implement a reference monitor which checks the proof and returns the check results to the application.

Browser extension

We developed a Chrome 1 extension. This extension intercepts policies from web applications at step (2) in Figure 4. With the policy, the extension then invokes a library Sage.js, which is a JavaScript implementation of Sage. Obtaining the proofs, the extension selects one proof and re-sends the request to the web application. Note that we leave the investigation of proof selection as future work. Alternatively, one may write client-side scripts to construct proofs. This will remove the need of a browser extension. However, based on our experiences, a browser extension could use more computational resources and thus lead to better performance. Hence, we chose the extension over client-side scripts.

Reference monitor

We chose to implement a reference monitor for Ruby on Rails 2 (or Rails in short) applications. This choice is motivated by the use of model-view-controller pattern of Rails applications. In such a pattern, the notion of resources are directly linked to that of models; each resource is associated with a model. This logical connection between resources and models provides an entry point for incorporating a reference monitor. Also, at the code level, the separation of the view of resources from the model enables us to introduce custom methods to intercept resource requests.

Function-wise, our reference monitor maintains a relation between resources and policies that should be proved in order to access the respective resources. The monitor also enforces the policies by checking proofs of the policies provided by 1 https://www.google.com/chrome/browser/ 2 http://rubyonrails.org/ each requester. To make the monitor effective, we modify Rails controllers which handle authorization logics. We implemented a reference monitor for Browser-CMS3 as a case study.

Experiments

We evaluated the performance of our Javascript implementation of the algorithm Sage with synthetic credentials. The experimental results demonstrate the efficiency of Sage. We first describe a generator we used to synthesize credentials for experiments. Then, we present the experimental results.

Credential generator

In order to generate credentials, we make use of a template of credentials available for proving p in r for randomly chosen principal p and role r . In a template, leaf nodes are labeled "sm", indicating simple membership credentials shall be generated, and non-leaf nodes are labeled "sc", "ic", or "lc", indicating the other three types of credentials shall be generated, respectively. A template with a root node rn means that a proof (p, r, c, s) can be obtained where c is a type rn credential and rn has a child node ch corresponding to a sub-proof (p , r , c , s ) in s such that c is a type ch credential. Then random, concrete credentials are generated whenever a node is reached when traversing a template. In addition, we also generate some "noisy" credentials which are useless for proving p in r.

The generator takes as input four parameters: (1) a tree template, (2) the height of a tree, (3) variant: the number of credentials that shall be created for each type of credentials at each node of the template, and (4) the number of noisy credentials. The generator outputs, in addition to credentials, the following parameters: the size of a generated credential set (i.e., the number of credentials in the set) and the number of credentials of each type in a credential set.

Experimental credential sets

We generated credentials by letting, all uniformly, the template be one of templates in Figure 6, height range from 1 to 5, the number of variant be 1 or 2, and the number of noisy credentials range from 0 to 20. We obtained 945 generated credential sets in total and used them as input to Sage. Note that the templates cover example policies like "Co-workers can see all photos and music" in the case studies of [START_REF] Mazurek | Toward strong, usable access control for shared distributed data[END_REF].

Figure 7 shows the distribution of the size of the generated credential sets, when the size is smaller than 200. The most of the generated credentials sets have a size smaller than 80. On the other hand, for the ranges between 80 and 180, each range contains 2-10 credentials sets. Also, there are 147 generated credential sets whose size is larger than 200.

Experimental results

For each of the 945 generated credential sets, we invoked Sage, which is implemented as a JavaScript library, to compute all constraint-compliant proofs of p in r, where p and r were chosen when generating the credential set. For each credential set, we attached usage constraints to 30% of the credentials in the set: half are delegation depth constraints and the other half are final-usage constraints. The experiments were performed on a machine with 8 GB 1600 MHz DDR3 memory and Intel Core i5-3570 3.4 GHz RAM.

Figure 8 shows the time Sage took to return proof sets for each generated credential set. When the size of the credential sets is smaller than 100, the time is less than 1 ms, with four exceptions. When the size is smaller than 200, the time is always less than 10 ms. And when the size is smaller than 1000, the time is always less than 100 ms. In all cases, the time is less than 1 second. The computation time grows exponentially with the size of the credential sets. However, assuming the size of credential sets used in practice is smaller than 1000, the overhead, being less than 100 ms, is moderate. The size of credential sets The averaged computation time (ms) Figure 8: The time Sage took to return proof sets Figure 9 depicts the time Sage took with respect to the size of the returned proof sets. The time increases exponentially with the size of the proof sets. However, when the size is smaller than 1000, the time is less than 100 ms, which we think is moderate. When the size is smaller than 10, the time is less than 1 ms except for two cases. When the size is smaller than 100, the time is less than 10 ms. In all cases, the computation time is less than 1 second.

Figure 10 shows the impact of noisy credentials on the computation time. In the figure, the computation time is the average of the time needed for the generated credential sets of the same size. The ratio of noisy credentials in the generated credential sets ranges from 0% to 50%. When the ratio is greater than 10%, the computation time is less than 100 ms. In all cases of the ratios, the time increases along with the growth of the size of the credential sets. Comparing the ratios, however, it appears that the higher the ratio is, the less computation time Sage took on average; the reason for this remains unclear to us.

Related Work and Conclusion

Seamons et al. [START_REF] Seamons | Requirements for policy languages for trust negotiation[END_REF] define two variants of the compliance checking problem: type-1 and type-2. The type-1 problem is to determine whether a policy is entailed by a set of credentials. The type-2 problem is to find a proof of a policy together with the used credentials in the proof. Lee and Winslett [4] propose a type-3 compliance checking problem -find all minimal proofs of a policy for a given set of credentials. While an algorithm for the type-2 problem shall be more efficient than an algorithm for the type-3 problem, the latter enables to apply strategies to proof and credential disclosure. This is also the main reason why we address a variant of the type-3 problem. The size of returned proof sets The computation time (ms) This variant of the type-3 problem is different in that we construct all constraint-compliant proofs of a policy. With respect to usage constraints on credentials, this work shares the same problem with [START_REF] Hu | Compliance checking for usage-constrained credentials in trust negotiation systems[END_REF]. While Hu et al. propose a solution by encoding credentials in answer set programming, we develop a novel algorithm and implement it for web applications. Unlike [START_REF] Lee | Towards an efficient and language-agnostic compliance checker for trust negotiation systems[END_REF] and [START_REF] Hu | Compliance checking for usage-constrained credentials in trust negotiation systems[END_REF], this work did not consider searching only minimal proofs of a policy. Concerning usage constraints on credentials, Bauer et al. [START_REF] Bauer | Constraining credential usage in logic-based access control[END_REF] propose an approach for proof-carrying authorization. It is not clear how to generate all constraint-compliant proofs with their approach. Approaches to CBAC for web applications include, for ex-ample, [START_REF] Bauer | Access Control for the Web via Proof-carrying Authorization[END_REF][START_REF] Vimercati | Integrating trust management and access control in data-intensive web applications[END_REF]. However, neither of them addresses enforcing usage constraints on credentials.

We have presented a new algorithm for constructing constraint-compliant policy proofs. We have proved the correctness of the algorithm and shown its efficiency by experiments. The algorithm is implemented as a JavaScript library, used in a browser extension, and integrated for an example Ruby on Rails application.

allows a principal to obtain the head role if the principal is assigned to all roles in the body.

If c is a linking containment credential, Handle-LC is called. First, in line 4, all principals who define a role using the linked role term are traversed. For each such principal, Construct-Proofs is called in line 5 to calculate proofs showing the principal is assigned to the defining role of c, which are assigned to the variable dp. If there exist proofs of this form, i.e., if dp is non-empty, Construct-Proofs is called again for the actual principal and the linked role, and the result is assigned to the variable lp. Then, in line 8, the Cartesian product of dp and lp is calculated and later returned.

Figure 1 :

 1 Figure 1: The inference rules for RT0 credentials.

Figure 3 :

 3 Figure 3: The Sage algorithm for constructing constraint-compliant proofs.

Figure 4 :

 4 Figure 4: The proposed architecture of CBAC in web applications.

Figure 6 :Figure 7 :

 67 Figure 6: Templates that were used to generate credentials

Figure 9 : 3 5 Figure 10 :

 93510 Figure 9: The time Sage took when the size of returned proof sets varies

  ∅) is a base proof of p in r based on CS if c is a simple membership credential r ← p. We say (p, r, c, s) is a proof of p in r based on CS if either it is a base proof or s is a set of proofs based on CS, called sub-proofs, such that for any (p i , r i , c i , s i ) ∈ s, (1) there exists c ∈ CS such that

	niv.network ← U niv.guest	U niv.guest ← U niv.P rof.collaborator
	U niv.P rof ← Bob	Bob.collaborator ← Alice
	Definition 1 (Proofs). Given a principal p, a role r, and a set CS of creden-
	tials, we say a tuple (p, r, c, p 1 in r 1 . . . p k in r k c p in r	l
	for some l ∈ {sm, sc, lc, ic} and (2) (p i , r i , c i , s i ) is also a proof based on CS.

http://www.browsercms.org/

Acknowledgments This work was supported by CASED (www.cased.de).

A The helper functions

This appendix lists the helper functions that are called by the Sage algorithm in Figure 3. More details of the algorihtm can be found on authors' website.

Handle-SC(c, p, nodes, rolepath, cons) 1 return Construct-Proofs(Body(c), p, nodes, rolepath, cons)

Handle-IC(c, p, nodes, rolepath, cons) If c is an intersection containment credential, Handle-IC is called. In lines 3 -4, for every role in the intersection of the body of c proofs are created by evaluating Construct-Proofs and then assigned to the variable ip. Finally, in lines 5 -7, the Cartesian product of all proofs in ip is calculated. Note that the Cartesian product is used to model that an intersection containment credential


Quoc Huy Do
email: do@cs.tu-darmstadt.de

Richard Bubel
email: bubel@cs.tu-darmstadt.de

Reiner Hähnle
email: haehnle@cs.tu-darmstadt.de

Exploit Generation for Information Flow Leaks in Object-Oriented Programs *

Keywords: test generation, symbolic execution, information flow

We present a method to generate automatically exploits for information flow leaks in object-oriented programs. Our approach combines self-composition and symbolic execution to compose an insecurity formula for a given information flow policy and a specification of the security level of the program locations. The insecurity formula gives then rise to a model which is used to generate input data for the exploit. A prototype tool called KEG implementing the described approach for Java programs has been developed, which generates exploits as executable JUnit tests.

Introduction

Analyzing programs to ensure that they do not leak secrets is necessary to improve confidence in the ability of a system to not put the security and privacy of its users at stake.

Information flow analysis is concerned with one aspect of this task, namely, to ensure that an outside agent with well-defined properties cannot learn secrets by observing (and initiating) several runs of a program. The nature of the secrets to be protected is specified by an information flow policy. The strongest one is noninterference, which does not allow the attacker to learn any kind of information about the secret. This is often too strong, e.g., an authentication program leaks the information whether an entered password is correct, hence, other policies like declassification (see [START_REF] Sabelfeld | Declassification: Dimensions and Principles[END_REF] for a survey) exist that allow to specify what kind of information may be released.

Several approaches to analyze programs for secure information flow relative to a given information flow policy exist. Many of these are either type-based [START_REF] Volpano | A Sound Type System for Secure Flow Analysis[END_REF][START_REF] Sabelfeld | A Model for Delimited Information Release[END_REF][START_REF] Hunt | On Flow-Sensitive Security Types[END_REF][START_REF] Myers | JFlow: Practical Mostly-Static Information Flow Control[END_REF][START_REF] Banerjee | Stack-based Access Control and Secure Information Flow[END_REF] or logic-based [START_REF] Darvas | A Theorem Proving Approach to Analysis of Secure Information Flow[END_REF][START_REF] Barthe | Secure Information Flow by Self-Composition[END_REF][START_REF] Scheben | Verification of Information Flow Properties of Java Programs without Approximations[END_REF]. In this paper we use a logic-based approach with self-composition (first introduced in [START_REF] Darvas | A theorem proving approach to analysis of secure information flow[END_REF]; the name self-composition was coined in [START_REF] Barthe | Secure Information Flow by Self-Composition[END_REF]), but our focus is not to verify that a program has secure information flow; instead we approach the problem from a bug finding point of view. For a given program we try to automatically generate exploits that demonstrate unintended information flows. Exploits are small programs that run the program of interest multiple times and report whether they could observe a leak. The generated exploits are well-structured and support the developer in identifying the origin of the leak and in understanding its nature.

To generate exploits we build on work from test generation [START_REF] Engel | Generating Unit Tests from Formal Proofs[END_REF][START_REF] King | Symbolic Execution and Program Testing[END_REF] with symbolic execution. Our implementation outputs the found exploits as JUnit tests such that the test fails if the program is insecure. The exploits can thus easily be added to a regression test suite.

The paper is structured as follows: Sect. 2 introduces basic notions and techniques. Sect. 3 explains the logic formalization of insecurity for noninterference and delimited information release. In Sect. [START_REF] Banerjee | Stack-based Access Control and Secure Information Flow[END_REF] we discuss the analysis of programs containing loops and method invocations. Sect. 5 presents our tool KEG and demonstrates the viability with case studies. We compare our work with others in Sect. [START_REF] Barthe | Secure Information Flow by Self-Composition[END_REF] and conclude with Sect. 7.

Background

Information Flow Policies

To analyze that a program does not leak confidential information, we need to define the security level of the program locations (program variables and fields) as well as an information flow policy which defines whether and what kind of information may flow between program locations of a different security level.

In this subsection we recapture the definitions of two well-known information flow policies which are supported by our approach.

Noninterference. Noninterference [START_REF] Cohen | Information Transmission in Sequential Programs[END_REF][START_REF] Volpano | A Sound Type System for Secure Flow Analysis[END_REF] is the strongest possible information flow policy. It prohibits any information flow from program locations containing confidential information (high variables) to publicly observable program locations (low variables); the opposite direction is allowed. As we consider only deterministic programs, noninterference can be easily formalized by comparing two program runs:

A program has secure information flow with respect to noninterference, if any two executions of the program starting in initial states with identical values of the low variables, also end in final states which coincide on the values of the low variables.

Let p denote a program and Var the set of all program variables of p.

(v) = σ 2 (v) for all v ∈ V .
A concrete execution trace τ of a program p is a possibly infinite sequence of program states τ = σ 0 σ 1 . . . produced by starting p in state σ 0 . In this paper, we are only concerned with terminating programs, and consequently, all of our execution traces are finite. Thus, we represent a concrete execution X of a program p as tuple σ X , σ X out , where σ X ∈ States p is the initial program state and σ X out ∈ States p is the final program state. The set of all possible concrete executions of p is denoted as Exc p .

We can now define the noninterference property as follows:

Definition 3 (Noninterference). Given a noninterference policy NI = (L, H) where L ∪ H = Var s.t. L contains the low variables and H the high variables.

A program p has secure information flow with respect to NI iff. for all concrete executions

X, Y ∈ Exc p it holds that if σ X L σ Y then σ X out L σ Y out .
Declassification. For many practical cases noninterference is too strict. E.g., a login program leaks usually the information whether an entered password is correct; or a database may be queried for aggregated information like the average salary of the employees, but not for the income of an individual employee.

Declassification is a class of information flow policies which allows to express that some confidential information may be leaked under specific conditions. The paper [START_REF] Sabelfeld | Declassification: Dimensions and Principles[END_REF] provides an extensive survey of declassification approaches.

In this paper we focus on delimited information release as introduced in [START_REF] Sabelfeld | A Model for Delimited Information Release[END_REF]. Delimited information release is a declassification policy which allows to specify what kind of information may be released. To this end so called escape hatch expressions are specified in addition to the security level of the program locations. For instance, the escape hatch e∈Employees salary(e) |Employees| can be used to declassify the average of the income of all employees. The formal definition of delimited information release is similar to Def. 3: Definition 4 (Delimited Information Release). Given a delimited information release policy Decl = (L, H, E) with L, H as before and E denoting a set of escape hatch expressions.

A program p has secure information flow with respect to Decl iff. for all concrete executions X, Y ∈ Exc p it holds that if σ X L σ Y and for all e ∈ E :

[[e]] σ X = [[e]] σ Y then σ X out L σ Y out . The expression [[e]
] σ denotes the semantic evaluation of e in state σ.

Logic-Based Information Flow Analysis

Symbolic Execution. Symbolic Execution [START_REF] King | Symbolic Execution and Program Testing[END_REF] is a versatile technique used for various static program analyses. Symbolic execution of a program means to run it with symbolic input values instead of concrete ones. Such a run results in a tree of symbolic execution traces, which covers all possible concrete executions. Each node in a symbolic execution tree is annotated by its symbolic state. In the example shown in Fig. 1b, the root node is a branching node whose outgoing edges are annotated by their branch conditions. Here the symbolic execution splits into two branches: the left one for the case where the symbolic value x 0 is non-negative and the right one for a negative x 0 . Both branches might be possible as we do not have any further information about the value of x 0 . The path condition pc i of a path sp i is the conjunction of all its branch conditions and characterizes the symbolic execution path uniquely. As long as the program does not contain loops or method invocations, a path condition is a quantifierfree formula in first order logic.

From the above tree we can extract that in case of a non-negative input value for x, the program terminates in a final state in which the final value of x remains unchanged (i.e., x 0 ) while the final value of y is 2(y 0 -1).

We fix the following notations as convention: Given a path i we refer to its path condition by pc i and to the final value of a program variable v ∈ Var by f v i . If we want to make explicit that the final value of a program variable v depends on the symbolic input value of a program variable u we pass it as an argument to f v i . For instance, f y 0 (x 0 , y 0 ) := 2(y 0 -1) in case of the final value of y on the left branch.

In case of unbounded loops or unbounded recursive method calls a symbolic execution tree is no longer finite. We overcome this obstacle and achieve a finite representation by making use of specifications as proposed in [START_REF] Hentschel | Visualizing Unbounded Symbolic Execution[END_REF]. This approach uses loop invariants and method contracts to describe the effect of loops and method calls. The basic idea is that loop invariants and method contracts contribute to path conditions and to the representation of the symbolic state. The approach has been implemented as a symbolic execution engine based on the verification system KeY [START_REF] Beckert | Verification of Object-oriented Software: The KeY Approach[END_REF], which we use as backend for the exploit generation presented in this paper.

Self-composition. Our exploit generation approach is derived from a logic-based formalization of noninterference using self-composition as introduced in [START_REF] Darvas | A theorem proving approach to analysis of secure information flow[END_REF][START_REF] Darvas | A Theorem Proving Approach to Analysis of Secure Information Flow[END_REF], based on a direct semantic encoding of noninterference in a program logic. The Hoare triple {Pre} p {Post} is valid iff. the program p started in any initial state that satisfies formula Pre terminates, then formula Post must hold in the reached final state. The semantic definition of noninterference as given in Definition 3 requires the comparison of two program runs. The authors of [START_REF] Darvas | A Theorem Proving Approach to Analysis of Secure Information Flow[END_REF] achieve this by copying the analyzed program and replacing all variables with fresh ones, such that the original and the copied program version do not share any memory. In more detail, let p(l,h) be the original program with l ∈ L, h ∈ H being the only program variables occurring in program p. Further, let p(l',h') represent the copied program constructed from p by renaming variable l to l and h to h .

Then {l . = l'}p(l,h); p(l',h'){l . = l'}
is a direct formalization of noninterference. A major drawback of the formalization is that it requires program p to be analyzed twice. Several refinements have been presented since then to avoid the repeated program execution [START_REF] Terauchi | Secure information flow as a safety problem[END_REF][START_REF] Barthe | Relational Verification Using Product Programs[END_REF]. We make use of an approach based on symbolic execution. The fundamental idea is to execute the program symbolically only once and then to use the path conditions and symbolic states to construct a single first-order formula with the same meaning as the Hoare Triple. To express the noninterference property, we simply copy path conditions and symbolic values, replacing the symbolic input values with fresh copies.

3 Exploit Generation for Insecure Programs

Logic Characterization of Insecurity

Our objective is to generate an exploit for a given program p which demonstrates that p is insecure with respect to a specified information flow policy. The basic idea is that the exploit runs p twice and throws an exception if an unintended information flow is detected. The problem that needs to be solved is how to find the initial states for both runs such that an information leak can be observed.

To this end we construct a first-order formula which is satisfiable, if the program is insecure. The formula is constructed in such a way that any satisfying model can be directly used to construct the required initial states.

For noninterference, as defined in Def. 3, that formula is constructed as follows: Let NI = (L, H) denote the noninterference policy with low variables L and high variables H. Each path sp i (i ∈ {0, . . . , n -1}) in the symbolic execution tree of p is uniquely characterized by its path condition pc i (L, H).

To represent two independent program runs, we create a copy of all program variables Var = {v | v ∈ Var } and obtain the sets L and H as copies of L and H, i.e., L = {l | l ∈ L} (analogously H ). Intuitively, the first run is performed using Var , while the second one uses the copy Var . Both runs are independent as they do not share any common memory. Then the NI-insecurity formula

0≤i≤j<n l∈L,l ∈L l . = l ∧ pc i (L, H) ∧ pc j (L , H ) ∧ l∈L f l i (L, H) . = f l j (L , H ) (1)
is satisfied iff. there is a model (i.e., state) σ assigning values to the program variables L, L , H, H such that there exist two paths i, j (i = j possible) with identical low level input, consistent path conditions (i.e., both paths can actually be taken), but for which the final value of at least one low level variable differs.

In other words, the model σ assigns concrete values to L, L , H and H such that p produces different low level output for two runs from initial states with identical low level input. (Formula (1) can be made more succinct by replacing L with L and omitting the first conjunct, which states L . = L .)

Example 1. The insecurity formula (1) for the example program from Fig. 1 and the NI policy L = {y}, H = {x} becomes

x 0 ≥ 0 ∧ x 0 ≥ 0 ∧ 2(y 0 -1) . = 2(y 0 -1) ∨ x 0 ≥ 0 ∧ x 0 < 0 ∧ 2(y 0 -1) . = 2(y 0 + 1) ∨ x 0 < 0 ∧ x 0 < 0 ∧ 2(y 0 + 1) . = 2(y 0 + 1)
It is easy to see that the first and third disjunct are unsatisfiable, but the second disjunct is satisfiable, e.g., for the model

x 0 → 0, x 0 → -1, y 0 → 1.
The NI-insecurity formula (1) can be rewritten into the equivalent formula

l∈L 0≤i≤j<n Leak(H,L,l,i,j) v∈L,v ∈L v . = v ∧ pc i (L, H) ∧ pc j (L , H ) ∧ f l i (L, H) . = f l j (L , H ) (2)
which helps us later to incorporate declassification. The formula Leak(H, L, l, i, j) allows to ascribe leaks to a specific target, i.e., it is satisfiable, if some information is leaked from the program variables in H to variable l.

Target Conditional Delimited Release

We extend the insecurity formula for noninterference (2) to delimited information release (DIR) [START_REF] Sabelfeld | A Model for Delimited Information Release[END_REF]. In addition to the standard version of DIR, our policy describes not only what information might be released by using escape hatches, but it also allows to express under which condition and to whom (target) the information might be leaked. The formula coincides for locations l ∈ L that are not allowed release targets (i.e., l ∈ T ) with the noninterference insecurity formula. Otherwise, the new second conjunct adds

C(Var ) ∧ C(Var ) → e(Var ) = e(Var )
as an additional restriction to the initial states for both runs, namely, that if both initial states satisfy the declassification condition C then they must also coincide on the value of the escape hatch expression. The rationale is that if there are two runs s.t. their respective initial state coincides on the low level input and on the escape hatches and if the final value for an allowed target differs, then more information than just the escape hatch must have been released.

The generalization of the above formula to more than one triple is straightforward and omitted for space reasons.

Exploit Generation using Program Specifications

In this section we discuss how to use program specifications like loop invariants and method contracts to analyze and generate exploits for programs involving unbounded loops or recursive method calls. These specifications need to be userprovided at the moment, but work on automatic generation of specifications is ongoing. We focus on the noninterference analysis case, the extension to declassification is straightforward.

Loop Specification

The path conditions pc for a program p are computed by symbolic execution of p. The problem to solve is how to symbolically execute a loop. In case a fixed bound is known a priori the loop can simply be unwound, but this is impractical if the bound is large and not possible at all for unbounded loops.

In program verification, loops are handled by providing a loop specification. A loop specification LS = (I, mod ) consists of a loop invariant formula I and a set of program variables mod which contains all program variables the loop is allowed to modify. In [START_REF] Hentschel | Visualizing Unbounded Symbolic Execution[END_REF] it is shown how to use such a specification for symbolic execution and we can simply reuse that option in our setting.

In the following we describe briefly how a loop specification is reflected in the NI-insecurity formula. Let b be the loop guard and LS = (I, mod ) the loop specification. The basic idea in [START_REF] Hentschel | Visualizing Unbounded Symbolic Execution[END_REF] is that the loop specification describes the state after exiting the loop. This means, we can treat the loop as a black-box and continue execution after the loop in a state for which the variables mod that might have been modified by the loop are set to an unknown value. Unknown values are represented by the set of fresh symbolic variables V mod . The only knowledge about the values of these variables is provided by the loop invariant and by the fact the loop guard b must be false (as we exited the loop).

Our insecurity formulas are always expressed as a constraint over the initial state. For instance, the final value f l i of variable l is given in terms of the initial symbolic values of the program variables. The same holds for the path conditions. We make this implicit weakest precondition computation here explicit for the loop guard and the invariant, i.e., I wp is the weakest precondition of I computed in the state directly after the loop (similar for the loop guard).

For the sake of simplicity, we only show how to adapt Leak(H, L, l, i, j) for the case that both paths i, j contain the same loop:

Leak(H, L, l, i, j) ≡ ( v∈L v = v ) ∧ pc i (V S ) ∧ pc j (V S ) ∧ (I wp (V S ) ∧ ¬b wp (V S )) ∧ (I wp (V S ) ∧ ¬b wp (V S )) ∧ f l i (V S ) = f l j (V S ) (4
) where b wp (V S ) is the symbolic value of the guard after the loop, V S = Var ∪ V mod . If one or both of paths i, j do not contain this loop, or have other loops, corresponding conjuncts are omitted or added accordingly.

Example 2. We illustrate formula (4). Consider the loop below with low variable l and high variable h. The loop specification is given as (I : l ≥ 0, mod : {l})

1 l = h * h; 2 while (l > 0) { l = l -1; } 3 l = l + h;
Let l mod , l mod be the fresh values representing the value of l directly after the loop. Computing the weakest precondition of the invariant gives us l mod ≥ 0 and for the guard l mod > 0 for the first run (analog for the second run). The resulting formula is:

l = l ∧ (l mod ≥ 0 ∧ ¬(l mod > 0)) ∧ (l mod ≥ 0 ∧ ¬(l mod > 0)) ∧ l mod + h = l mod + h
The formula is satisfiable for l = l = 10, l mod = l mod = 0, h = 1 and h = 2. And actually the program is insecure. Removing the last statement would make it secure and the formula unsatisfiable as the comparison of the final values would change to l mod = l mod which would be unsatisfiable.

Method Contracts

Let m denote a method. A contract C m for m is a triple (Pre m , Post m , Mod m ) with precondition Pre m , postcondition Post m and modifies (or assignable) clause Mod m , which enumerates all program variables that m is allowed to change.

A method satisfies its contract, if it ensures that when invoked in a state for which the precondition is satisfied, then in the reached final state the postcondition holds and at most the program variables (locations) listed in the assignable clause have been modified.

Analysing Noninterference w.r.t. to a Precondition. Given a method m with contract C m . We want to analyze whether m respects its noninterference policy NI = (L, H) under the condition that m is only invoked in states satisfying its precondition Pre m . Changing the noninterference formula ( 2) is easy and only requires adding a restriction to the initial states requiring them to satisfy the method's precondition:

Leak(H, L, l, i, j) ∧ P re m (L, H) ∧ P re m (L , H ) (5)
Analyzing Programs for Noninterference using Method Contracts. A similar problem as for loops manifests itself when symbolically executing a program which invokes one or more methods. One solution is to replace the method invocation by the body of the invoked method. If the methods are small this is a viable solution, but it is impractical if the invoked method is complex and is even impossible for recursive methods without a fixed maximal recursion depth. This problem is solved in [START_REF] Hentschel | Visualizing Unbounded Symbolic Execution[END_REF] by using method contracts in a similar way loop specifications have been used. Instead of a loop invariant, the pre-and postconditions become parts of the path conditions. The modifies clause gives again rise to fresh variables used to represent the symbolic value of the program variables that might have been changed as side-effect of the method invocation.

Let m be the method that is analyzed for secure information flow and which invokes a method n. The method contract of n is given as (Pre n , Post n , Mod n ). For the case that both two paths i, j contain one method call for n we get:

Leak(H, L, l, i, j) ≡ ( v∈L v = v )∧pc i (V S )∧pc j (V S )∧(Pre wp n (V S )∧Post wp n (V S )) ∧ (Pre wp n (V S ) ∧ Post wp n (V S )) ∧ f l i (V S ) = f l j (V S ) (6)
where V S is the set of program variables extended by the newly introduced variables resulting from the modifies clause of method n and Pre wp n , Post wp n are the weakest preconditions of Pre n , Post n computed directly before (resp. after) the method invocation. The general case is similar to loops.

General Observations and Remarks

Using loop specifications or method contracts has one major drawback, namely, that not all models of a formula give rise to an actual information leak, or even worse, the insecurity formula of a secure program might become satisfiable. This case does not effect the soundness, but triggers false warnings. The reason is that the specifications might be too weak and allow behaviours that are not possible in the actual program. These false warnings can be filtered out by actually running

Symbolically execute method

Compose all insecurity formulas

Find models satisfying formulas Generate JUnit tests from found models Fig. 2: Exploit Generation by KEG the generated exploit. If the exploit fails to demonstrate the information leak, we know that our model was a spurious one. We can even start a feedback loop with a conflict clause which rules out the previously found model.

On the other side if loop or method specifications are not just too weak, but wrong in the sense that they exclude existing behaviour, leaks might not be detected. This can be avoided by verifying the specifications using a program verification tool. As we are concerned with bug detection and not verification, this case is not too bad as we do not claim to find all bugs.

Implementation and Experiments

The KeY Exploit Generation Tool

We implemented our approach as a tool called KeY Exploit Generation (KEG) 1 based on the verification system KeY for Java [START_REF] Beckert | Verification of Object-oriented Software: The KeY Approach[END_REF]. KEG uses KeY as symbolic execution (SE) engine, which supports method and loop specifications to achieve a finite SE tree. The SMT solver Z3 is used to find models for the insecurity formulas. KEG is able to deal with object types and arrays (to some extent).

Fig. 2 outlines KEG's work-flow. As starting point it serves a Java method m which is analysed for secure information flow w.r.t. a given information flow specification. First, method m is symbolically executed (using KeY) to obtain the SE tree with the method's path conditions and the final symbolic values of the program locations modified by m. Using this information the insecurity formulas are generated and given to a model finder (in our case the SMT solver Z3). If a model for the insecurity formula has been found, the model is used to determine the initial states of two runs which exhibit a forbidden information flow. The generated exploit sets then up two runs (one for each initial state) and inspects the reached final states to detect a leak. KEG outputs the exploited program as a JUnit test to be included into a regression test suite.

Exploit Generation Using a Simple Example

We explain KEG using the simple example shown below: Class Simple contains three integer typed fields l, x and y as well as a method called magic() which assigns a value to l depending on the sign of field x. The information flow policy is annotated as special comment types. Line 3 is a class level specification and forbids any information flow from x and y to l. Hence, here x and y are high variables and l is a low variable. However, this strict noninterference policy is relaxed in line 5 for method magic() by providing a target conditional release specification consisting of an escape hatch (x * y), the target l and the condition x>-1.

Running KEG on the above example produces a symbolic execution tree consisting of two paths; one for each branch of the conditional statement. KEG generates for each pair of these paths the corresponding insecurity formulas and passes them on to an SMT solver. Of the three generated insecurity formulas only one is satisfiable and Z3 provides a model:

Insecurity Formula Model

(let ((a!1 (not (and (> self_x_1 (-1)) (> self_x_2 (-1)))))) (and (>= self_x_1 1) (<= self_x_2 0) (or (not

(= self_x_1 self_x_2)) (not (= self_y_1 self_y_2))) (= self_l_1 self_l_2) (not (= ( * self_y_1 self_x_1) 0)) (or a!1 (= ( * self_x_1 self_y_1) ( * self_x_2 self_y_2))))) self_x_1 : 1 self_x_2 : -1 self_y_1 : -1 self_y_2 : 1 self_l_1 : 0 self_l_2 : 0
The formula comparing two runs which take different branches of the conditional statement and thus leak the sign of field x. KEG generates exactly one exploit, which is output as a well-structured and human readable JUnit test.

Experiments

We performed a number of small experiments2 for a first evaluation of our approach. Table 1 shows the aggregated results. All experiments were done on an Intel Core i7-4702HQ processor with JVM setting -Xmx4096m.

Concerning the runtime performance: A significant amount is spent for parsing the program, this can be reduced by parser optimizations, e.g., by using a hand-coded version instead of a generated parser. Model finding time can be optimized by performing simple techniques like symmetry reduction, learning and caching, all of which have not yet been implemented. Another factor is the programming language Java whose optimizations are performed at runtime and, hence, code run only a few times will not be optimized at all.

A few observations concerning some of the concrete case studies: For the examples Mul and Comp, we analyzed also the effect of loop specifications resp. method specifications in case of strong, weak and wrong specifications (filename Strong/Weak/Wrong LI/MC). As expected in case of sufficiently strong specifications, all insecure paths could be identified and corresponding exploits have been generated. Weak specifications over-approximated possible behaviour leading to false warnings, while wrong specifications excluded actual behaviours and missed existings leaks. The analysis of method search in class ArrSearch identified the method correctly as secure with respect to the specified declassification policy and generated no exploits. Our approach to exploit generation is based on self-composition [START_REF] Darvas | A theorem proving approach to analysis of secure information flow[END_REF][START_REF] Barthe | Secure Information Flow by Self-Composition[END_REF][START_REF] Darvas | A Theorem Proving Approach to Analysis of Secure Information Flow[END_REF]. The paper [START_REF] Darvas | A Theorem Proving Approach to Analysis of Secure Information Flow[END_REF] addresses also declassification. Its authors observe that in their formalization it is possible to express and verify that a program is insecure. Our formalization of insecurity uses this observation. Exploit generation (extraction of models) in our paper owes to techniques developed for automatic test generation. In particular, we build upon work presented in [START_REF] King | Symbolic Execution and Program Testing[END_REF][START_REF] Engel | Generating Unit Tests from Formal Proofs[END_REF], where symbolic execution is used as a means to generate test cases for functional properties. Logic-based approaches such as [START_REF] Beckert | Information Flow in Object-Oriented Software[END_REF][START_REF] Scheben | Verification of Information Flow Properties of Java Programs without Approximations[END_REF] are fully precise and at the same time can flexibly express various information flow properties beyond the policies presented in this paper. The verification process is not fully automatic, however, and non-trivial interactions with the theorem prover are required. In [START_REF] Nanevski | Verification of Information Flow and Access Control Policies with Dependent Types[END_REF] higher order logic is used to express information flow properties for object-oriented programs, which is highly expressive, but poses also a high demand on user interaction.

Pairs of symbolic execution paths instead of standard self-composition have been independently used in [START_REF] Phan | Self-composition by Symbolic Execution[END_REF] to check programs for noninterference. However, the author is only concerned with checking noninterference, but does not support declassification. Unbounded loops and recursive methods are not addressed.

In [START_REF] Vaughan | Inference of expressive declassification policies[END_REF], leaks are inferred automatically and expressed in a human-readable security policy language helping programmers to decide whether the program is secure or not, however it can not give concrete counterexamples that could suggest further corrections. Counterexamples can be used not only to generate executable exploits as in our approach, but also to refine declassification policies quantifying the leakage [START_REF] Banerjee | What you lose is what you leak: Information leakage in declassification policies[END_REF][START_REF] Backes | Automatic discovery and quantification of information leaks[END_REF]. However, both above approaches do not provide a solution for unbounded loops and recursions.

ENCoVer [START_REF] Balliu | ENCoVer: Symbolic Exploration for Information Flow Security[END_REF] uses epistemic logic and makes use of symbolic execution (concolic testing) to check noninterference for Java programs. In [START_REF] Milushev | Noninterference via Symbolic Execution[END_REF], the authors proposed a tool which checks that a C program is secure w.r.t. noninterference. It transforms the original program and makes use of dynamic symbolic execution to analyze the program's information flow. Both tools check loops and recursive method invocations only up to a fixed depth.

Type-based approaches to information flow like [START_REF] Volpano | A Sound Type System for Secure Flow Analysis[END_REF][START_REF] Hunt | On Flow-Sensitive Security Types[END_REF][START_REF] Myers | JFlow: Practical Mostly-Static Information Flow Control[END_REF][START_REF] Sabelfeld | A Model for Delimited Information Release[END_REF] or those based on dependency graphs [START_REF] Graf | Using JOANA for Information Flow Control in Java Programs -A Practical Guide[END_REF] distinguish themselves by their high performance and ability to check large systems. Common drawbacks are lack of precision and resulting false warnings and/or restrictions on the syntactic form of a program.

None of the logic-based and type-based approaches to noninterference analysis mentioned above does generate exploits from a failed proof or analysis. Our work does not intend to replace their approaches, but to be used complementary.

Conclusion

We presented a novel approach for automatically detecting information flow leaks in object-oriented imperative programs. Exploits are generated based on satisfying models of insecurity formulas and output as tests so that they can easily be integrated into regression test collections. We also showed how program specifications such as loop invariants and method contracts can be used to overcome the obstacle of an infinite symbolic execution tree in case of unbounded program structures. We have built a prototypical tool (KEG) based on our approach that handles sequential Java programs and we applied it to a number of case studies.

We plan to integrate KEG with the abstraction framework presented in [START_REF] Wasser | A Theorem Prover Backed Approach to Array Abstraction[END_REF] which allows us to automatically generate loop invariant and method contracts to avoid the need for user-provided specifications.

Fig. 1 :

 1 Fig. 1: Program and its symbolic execution tree

Definition 5 (

 5 Target Conditional Delimited Release). Given a program p with Var being the set of all variables occurring in p and a noninterference policy NI = (L, H). A Target Conditional Delimited Release (TCD) policy (D, NI ) is a set of TCD specification triples where each triple (e, C, T ) ∈ D consists of an escape hatch expression (i.e., first order term) e over Var , a declassification condition formula C over Var and -T ⊆ L, a set of program variables to which the specified escape hatch is allowed to be leaked. A program satisfies a given TCD policy (D, NI ) if there is no information flow from H to L, except for the cases covered by a triple (e, C, T ) ∈ D which allows the program to release the information captured by the escape hatch expression e to a location in T , if condition C is satisfied in the initial state of a program run. Given a TCD policy (D, NI ) and a program p. We give the insecurity formula for the case that D = {(e, C, T )} consists of a single TCD specification triple: l∈L Leak(H, L, l, i, j) ∧ ((l ∈ T ∧ C(Var ) ∧ C(Var )) → e(Var ) = e(Var )) (3)

1 public class Simple { 2 public 3 / 5 /

 235 int l; private int x, y; * ! l | x y ; ! * / 4 * @ escapes (x * y) \to l \if x>-1; @ * / 6 public void magic() { if(x>0) { l=x * y; } else { l=0; } } 7 } 1 www.se.tu-darmstadt.de/research/projects/albia/download/exploit-generation-tool

  T and D being the union of all concrete domains. The set of all states for a given program p is denoted as States p .Definition 2 (State Coincidence). Given a set of program variables V and two states σ 1 , σ 2 ∈ States p . We write σ 1 V σ 2 iff. σ 1 and σ 2 coincide on V , i.e., σ 1

	We define coincidence of program states w.r.t. a set of program variables:

Definition 1 (Program State). A program state σ maps each program variable v ∈ Var of type T to a value of its concrete domain D T , i.e., σ : Var → D with σ(v : T ) ∈ D

Table 1 :

 1 Case studies statistics

	File	Analyzed #L/MI Policy S/I TL TSE TMF	TTot #GE/FW
	name	Method		(NI/D)	(ms) (ms) (ms) (ms)
	Mul	product	0 / 0	D	I 4187 847 1188 6266 1 / 0
	Mul StrongLI	product	1 / 0	D	I 4275 1746 1211 7274 1 / 0
	Mul WeakLI	product	1 / 0	D	I 4214 1909 1293 7463 2 / 1
	Mul WrongLI	product	1 / 0	D	I 4397 1678 1169 7285 0 / 0
	Comp StrongMC doWork	0 / 1	NI	I 4181 1491 2278 7995 3 / 0
	Comp WeakMC doWork	0 / 1	NI	I 4217 1383 2417 8065 3 / 3
	Comp WrongMC doWork	0 / 1	NI	I 4182 1395 2275 7887 0 / 0
	Company	calculate 1 / 1	NI	I 4283 2496 1990 8816 3 / 0
	ExpList	magic	0 / 0	NI	I 4178 1911 2535 8668 1 / 0
	ExpLinkedList magic	0 / 4	NI	I 4229 4690 6564 15526 2 / 0
	ExpArrayList	magic	0 / 5	NI	I 4230 8975 11505 24752 3 / 0
	ArrMax	findMax 1 / 0	NI	I 4215 3584	963 8804 1 / 0
	ArrSearch	search	1 / 0	D	S 4199 2934 2400 9568 0 / 0

#(L/MI/GE/FW): nr of Loops/Method Invocations/Generated Exploits/False Warnings NI/D: Non-Interference/Declassification, S/I: Secure/Insecure T X : Time for Loading/Symbolic Execution/Model Finding/Total 6 Related Work

www.se.tu-darmstadt.de/fileadmin/user_upload/Group_SE/Tools/KEG/experiments.zip

The work has been funded by the DFG priority program 1496 "'Reliably Secure Software Systems'"


Jiang Ming

Dongpeng Xu

Dinghao Wu

Memoized Semantics-Based Binary Diffing with Application to Malware Lineage Inference

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

In many tasks of software security, the source code of the program under examination is typically absent. Instead, the executable binary itself is the only available resource to analyze. Therefore, determining the real differences between two executable binaries has a wide variety of applications, such as latent vulnerabilities exploration [START_REF] Heng Ng | A study on latent vulnerabilities[END_REF], automatic "1-day" exploit generation [START_REF] Brumley | Automatic patch-based exploit generation is possible: Techniques and implications[END_REF] and software plagiarism detection [START_REF] Luo | Semanticsbased obfuscation-resilient binary code similarity comparison with applications to software plagiarism detection[END_REF]. Conventional approaches can quickly locate syntactical differences by measuring instruction sequences [START_REF] Sikorski | Practical Malware Analysis: The Hands-On Guide to Dissecting Malicious Software[END_REF] or byte N-grams [START_REF] Kolter | Learning to detect malicious executables in the wild[END_REF]. However, such syntax-based comparison can be easily defeated by various obfuscation techniques, such as instruction substitution [START_REF] Jacob | The superdiversifier: Peephole individualization for software protection[END_REF], binary packing [START_REF] Roundy | Binary-code obfuscations in prevalent packer tools[END_REF] and self-modifying code [START_REF] Bruschi | Using code normalization for fighting self-mutating malware[END_REF]. The latest binary diffing approaches [START_REF] Gao | BinHunt: Automatically finding semantic differences in binary programs[END_REF][START_REF] Ming | iBinHunt: Binary hunting with interprocedural control flow[END_REF] simulate semantics of a snippet of binary code (e.g., basic block) by symbolic execution and represent the input-output relations as a set of symbolic formulas. Then the equivalence of formulas are verified by a constraint solver. Such logic-based comparison, capturing the intrinsic semantic differences, has been applied to finding differences of program versions [START_REF] Gao | BinHunt: Automatically finding semantic differences in binary programs[END_REF], comparing inter-procedural control flows [START_REF] Ming | iBinHunt: Binary hunting with interprocedural control flow[END_REF] and identifying code reuse [START_REF] Luo | Semanticsbased obfuscation-resilient binary code similarity comparison with applications to software plagiarism detection[END_REF][START_REF] Heng | Exposé: Discovering potential binary code reuse[END_REF].

On the other hand, malware authors frequently update their malicious code to circumvent security countermeasures. According to the latest annual report of Panda Security labs [START_REF]Annual report 2013 summary[END_REF], in 2013 alone, there are about 30 million malware samples in circulation and only 20% of them are newly created. Obviously, most of such malware samples are simple update (e.g., apply a new packer) to their previous versions. Therefore, hunting malware similarities is of great necessity. The nature of being resilient to instruction obfuscation makes semantics-based binary diffing an appealing choice to analyze highly obfuscated malware as well. Unfortunately, the significant overhead imposed by the state-of-the-art approach has severely restricted its application in large scale analysis, such as malware lineage inference [START_REF] Jang | Towards automatic software lineage inference[END_REF], which normally requires pair-wise comparison to identify relationships among malware variants. In this paper, we first diagnose the two key obstacles leading to the performance bottleneck, namely high invocations of constraint solver and slow symbolic execution.

To address both factors, we propose basic blocks fast matching by reusing previously compared results, which consists of three optimization methods to accelerate equivalent basic block matching. Our key insight is that malware variants are likely to share common code [START_REF] Lindorfer | Lines of malicious code: Insights into the malicious software industry[END_REF]; new variant may be just protected with a different packer or incremental updates. As a result, we exploit code similarity by adopting union-find set [START_REF] Thomas | Introduction to Algorithms[END_REF], an efficient tree-based data structure, to record semantically equivalent basic blocks which have already been identified. Essentially, the union-find structure stores the md5 value of each matched basic block after normalization. Maintaining the union-find structure during successive comparisons allows direct reuse of previous results, without the need for re-comparing them. Moreover, to further cut down the high invocation times of constraint solver, we purpose to concretize symbolic formulas and cache equivalence queries. We have implemented these optimizations on top of iBinHunt [START_REF] Ming | iBinHunt: Binary hunting with interprocedural control flow[END_REF] and evaluated them when performing malware lineage inference on 12 malware families. Our experimental results show that our methods can speed up malware lineage inference, symbolic execution and constraint solver by a factor of 4.4x, 4.0x and 4.3x, respectively. Our proposed solution focuses on accelerating basic blocks matching and therefore can be seamlessly woven into other binary diffing approaches based on equivalent basic blocks. In summary, the contributions of this paper are as follows:

1. We look into the high overhead problem of semantics-based binary diffing and identify cruxes leading to the performance bottleneck. 2. We propose basic blocks fast matching to enable more efficient binary comparison, including maintaining a union-find set structure, concretizing symbolic formulas and caching equivalence queries. 3. We implement our approach on a state-of-the-art binary diffing tool and demonstrate its efficacy in malware lineage inference.

The rest of the paper is organized as follows. Section 2 provides the background information. Section 3 studies the performance bottleneck of semantics-

Background

In this section, we introduce the background information of semantics-based binary diffing. The core method of current approaches [START_REF] Gao | BinHunt: Automatically finding semantic differences in binary programs[END_REF][START_REF] Ming | iBinHunt: Binary hunting with interprocedural control flow[END_REF][START_REF] Luo | Semanticsbased obfuscation-resilient binary code similarity comparison with applications to software plagiarism detection[END_REF] are matching semantically equivalent basic blocks. Basic block is a straight line code with only one entry point and only one exit point, which makes a basic block highly amenable to symbolic execution (e.g., without conjunction of path conditions). Fig. 1 presents a motivating example to illustrate how semantics of a basic block is simulated by symbolic execution. The two basic blocks in Fig. 1 are semantically equivalent, even though they have different x86 instructions (listed in bold). In practice, symbolic execution is performed on a RISC-like intermediate language (IL), which represents complicated x86 instructions as simple Single Static Assignment (SSA) style statements (e.g., ecx 0, edx 1).

Taken the inputs to the basic block as symbols, the output of symbolic execution is a set of formulas that represent input-output relations of the basic block. Now determining whether two basic blocks are equivalent in semantics boils down to find an equivalent mapping between output formulas. Note that due to obfuscation such as register renaming, basic blocks could use different registers or variables to provide the same functionality. Hence current approaches exhaustively try all possible pairs to find if there exists a bijective mapping

P i n g M i m a i l D e l f S

t a r t P a g e R a t i o o f p r o c e s s i n g t i m e ( % )

O t h e r s S E S T P Fig. 3. Ratio of processing time of iBinHunt between output formulas. Fig. 2 shows such formulas mapping attempt for the output formulas shown in Fig. 1. The "true" or "false" indicates the result of equivalence checking, such as whether edx 1 = eax 3. After 10 times comparisons, we identify a perfect matched permutation and therefore conclude that these two basic blocks are truly equivalent.

Based on the matched basic blocks, BinHunt [START_REF] Gao | BinHunt: Automatically finding semantic differences in binary programs[END_REF] computes the similarity of control flow graphs of two binaries by graph isomorphism; iBinHunt [START_REF] Ming | iBinHunt: Binary hunting with interprocedural control flow[END_REF] finds semantic differences between execution traces and Luo et al. [START_REF] Luo | Semanticsbased obfuscation-resilient binary code similarity comparison with applications to software plagiarism detection[END_REF] detect software plagiarism by matching "longest common subsequence of semantically equivalent basic blocks".

Performance Bottleneck

We look into the overhead imposed by semantics-based binary diffing and find that there are two factors dominating the cost. The first is the high number of invocations of constraint solver. Recall that current approaches check all possible permutations of output formulas mapping. The constraint solver will be invoked every time when verifying the equivalence of formulas. For example, two basic blocks in Fig. 1 have 3 symbolic formulas and 1 constant value respectively. As shown in Fig. 2, We have to employ constraint solver at most 9 times to find an equivalent mapping between 3 output formulas. Too frequently calling constraint solver incurs a significant performance penalty. The second is the slow processing speed of symbolic execution. Typically symbolic execution is much slower than native execution, because it simulates each x86 instruction by interpreting a sequence of IL statements.

To quantitatively study such performance bottleneck, we selected 4 malware families from our evaluation dataset (see Section 5.1): 3 families have large number of samples (StartPage, Delf and Mimail) and one family (Ping) has the maximal code size. We applied iBinHunt [START_REF] Ming | iBinHunt: Binary hunting with interprocedural control flow[END_REF] to compare execution traces of pair-wise samples within each family. The constraint solver we used is STP [START_REF] Ganesh | A decision procedure for bit-vectors and arrays[END_REF]. Fig. 3 shows the ratio of each stage's processing time on average: constraint solver solving time ("STP" bar), symbolic execution time ("SE" bar) and other operations ("Others" bar). Apparently, STP's processing time accounts for most of running time of iBinHunt (more than 50%). Experiments on EXE [START_REF] Cadar | EXE:automatically generating inputs of death[END_REF] and KLEE [START_REF] Cadar | KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs[END_REF] report similar results, in which running time is dominated by the constraint solving. Besides, the symbolic execution also takes up to about 23% running time. Thus, an immediate optimization goal is to mitigate too frequent invocations of constraint solver and slow symbolic execution.

Optimization

Union-Find Set of Equivalent Basic Blocks

When we compare malware variants to identify their relationships (a.k.a, lineage inference [START_REF] Jang | Towards automatic software lineage inference[END_REF]), our key observation is that similar malware variants are likely to share common code [START_REF] Lindorfer | Lines of malicious code: Insights into the malicious software industry[END_REF]. For example, all of the Email-Worm.Win32.NetSky samples in our dataset search for email addresses on the infected computer and use SMTP to send themselves as attachments to these addresses. The net result is we have to re-compare large number of basic blocks that have been previously analyzed. Therefore our first optimization is to utilize union-find set [START_REF] Thomas | Introduction to Algorithms[END_REF], an efficient tree-based data structure, to reuse previous matched equivalent basic blocks. More specifically, we first normalize basic blocks to ignore offsets that may change due to code relocation and some nop instructions. MD5 value of the byte sequence of each basic block is then calculated. Secondly, we dynamically maintain a set of union-find subsets to record semantically equivalent basic blocks, which are represented by their MD5 value. The basic blocks within the same subset are all semantically equivalent to each other. Next we'll discuss these two steps in detail.

Normalization Binary compiled from the same source code often have different address value caused by memory relocation during compilation. What's more, malware authors may intentionally insert some instruction idioms like nop and xchg eax, eax to mislead calculation of hash value. The purpose of normalization is to ignore such effects and make the hash value more general. Taken the basic block 2 in Fig. 1 as an example, Fig. 4 presents how to normalize a basic block, in which we replace address values with zeros and remove all nop statements. After that, the MD5 value of the basic block's byte sequence is calculated.

Maintain Union-Find Set We define the three major operations of union-find set as follows: The elements within a subset build up a tree structure. Find operation will always recursively traverse on the tree structure. However the tree structure might degrade to a long list of nodes, which incurs O(n) time in the worst case for Find. To avoid highly unbalanced searching tree, an improved path compression and weighted union algorithm are applied to speed up Find operation. Algorithm 1 shows the pseudo-code of MakeSet, Find and Union. MakeSet creates an initial set containing only one basic block. Path compression is a way to flatten the structure of the tree when Find recursively explores on it. As a result, each node's parent points to the root Find returns (Line 7). Weighted Union algorithm attaches the tree with smaller depth to the root of taller tree (Line 17, Line 20), which only increases depth when depths are equal (Line 24). Fig. 5 shows an example of maintaining an union-find set. Given previously matched basic block pairs (as shown in left most block), after initial MakeSet and Union operations, we get three subsets, that is, {a, b}, {c, d} and {e, f, g}. Then assuming b and c, two basic blocks coming from different subsets (subset 1 and 2), have the same semantics, that means all of the basic blocks in these two subsets are in fact equivalent. Therefore we perform weighed union and path compression to join the two subsets to a new subset (subset 4). The resulting tree is much flatter with a depth 1. After union, we can immediately determine that b and d are equivalent, even if these two basic blocks were not compared before. In addition to union-fine set, we also maintain a DiffMap to record two subsets that have been verified that they are not equivalent. As shown in the lower right side of Fig. 5, if we find out a and e are different, we can safely conclude that basic blocks in subset 4 are not equivalent to the ones in subset 3, without the need for comparing them anymore.

Algorithm 1 MakeSet, Find and Union

Concretizing Symbolic Formulas

Fig. 2 shows a drawback of semantics-based binary diffing: without knowing the mapping of output formulas for equivalence checking, current approaches have to exhaustively try all possible permutations. To ameliorate this issue, we introduce a sound heuristic that if two symbolic formulas are equivalent, they should generate equal values when substituting symbols with the same concrete value. Therefore we give preference to the symbolic formulas producing the same value after concretization. Taken the output formulas in Fig. 1 as example, we substitute all the input symbols with a single concrete value 1. In this way, we can quickly identify the possible mapping pairs and then we verify them again with STP. As a result, we only invoke STP 3 times, instead of 9 times as is previously done. Note that using STP for double-check is indispensable, as two symbolic formulas may happen to generate the same value. For example, i << 1 is equal to i * i when i = 2.

Caching Equivalence Queries

Besides, in order to further reduce the invocations of STP when possible, we manage a QueryMap to cache the result of equivalence queries, which is quite similar to constraints caching adopted by EXE [START_REF] Cadar | EXE:automatically generating inputs of death[END_REF] and KLEE [START_REF] Cadar | KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs[END_REF]. The key of QueryMap is MD5 value of an equivalence query, such as whether edx 1 = eax 3 if Find(a ) = Find(b ) then within the same subset 8:

return

Basic Blocks Fast Matching

We merge all three optimization methods discussed above together to comprise our basic blocks fast matching algorithm (as listed in Algorithm 2). Our basic blocks fast matching exploits syntactical information and previous result for early pruning. When comparing two basic blocks, we first normalize the basic blocks and compare their hash value (Line 4). This step quickly filters out basic blocks with quite similar instructions. If two hash values are not equal, we will identify whether they belong to the same union-find subset (Line 7). Basic blocks within the same subset are semantically equivalent to each other. If they are in the two different subsets, we continue to check DiffMap to find out whether these two subsets have been ensured not equivalent (Line 10). At last, we have to resort to comparing them with symbolic execution and STP, which is accurate but computationally more expensive. At the same time, we leverage heuristic of concretizing symbolic formulas and QueryMap cache to reduce the invocations of STP. After that we update union-find set and DiffMap accordingly (Line 15∼22).

5 Experimental Evaluation

Implementation and Experiment Setup

We have implemented our basic blocks fast matching algorithm on top of iBin-Hunt [START_REF] Ming | iBinHunt: Binary hunting with interprocedural control flow[END_REF], a binary diffing tool to find semantic differences between execution traces, with about 1, 800 Ocaml lines of code. The saving and loading of unionfind set, DiffMap and QueryMap are implemented using the Ocaml Marshal API, which encodes arbitrary data structures as sequences of bytes and then stores them in a disk file. We collected malware samples from VX Heavens 1 and leveraged an online malware scan service, VirusTotal 2 , to classify the samples into an initial 12 families. These malware samples range from simple virus to considerably large Trojan horse. The dataset statistics is shown in Table 1. The experimental data are collected during malware lineage inference within each family, that is, we perform pair-wise comparison to determine relationships among malware variants. The forth column of Table 1 lists the number of pair-wise comparison of each family and the total number is 1, 008. Our testbed consists of Intel Core i7-3770 processor (Quad Core with 3.40GHz) and 8GB memory. The malware execution traces are collected when running in Temu [START_REF] Yin | TEMU: Binary code analysis via whole-system layered annotative execution[END_REF], a whole-system emulator. Since most of malware are packed, we developed a generic unpacking plug-in to monitor malware sample's unpacking and start to record trace only when the execution reaches the original entry point (OEP) [START_REF] Liu | Denial-of-service attacks on host-based generic unpackers[END_REF].

Performance

Cumulative Effects We first quantify the effects of the set of optimizations we presented in our basic blocks fast matching algorithm (Algorithm 2). Fig. 6 shows the speedup of malware lineage inference within each family when applying optimizations cumulatively on iBinHunt. Our baseline for this experiment is a conventional iBinHunt without any optimization we proposed. The "O1" bar indicates the effect of normalization, which can quickly identify basic block pairs with the same byte sequences. Such simple normalization only achieve notable improvement on several families such as Ping and Bube, in which instructions are quite similar in syntax. The bar denoted as "O2", captures the effect of the unionfind set and DiffMap, which record previously compared results. Optimization O2 brings a significant speedup from 1.4x to 2.9x on average. Especially for some highly obfuscated malware families, such as Delf and Bagle, O2 outperforms O1 by a factor of up to 3.1. The "O3" bar, denoting concretizing symbolic formulas, introduces an improvement by 17% on average. Optimization of QueryMap (O4) offers an enhanced performance improvement by average 30% and with a peak value 46% to the NetSky. Particularly, since StartPage samples adopt different implementation ways to tamper with the startup page of Internet browsers, we observer quit large similarity distances among StartPage variants. In spite of this, our approach still accelerate the binary code diffing greatly.

Furthermore, we study the effect of our basic blocks fast matching over time. We choose Sasser to test because the impact of the optimizations on Sasser is close to the average value. As shown in Fig. 7, as the union-find set is enlarged and QueryMap is filled, our approach becomes more effective over time. The number of executed basic blocks is normalized so that data can be collected across intra-family comparisons.

Alleviate Performance Bottleneck In Section 3, we identified two factors that dominate the cost of semantics-based binary diffing: namely symbolic execution and constraint solver. In this experiment, we study the effect of our optimizations on these two performance bottlenecks. The column 2∼4 of Table 2 lists the average symbolic execution time and speedup before/after optimization when comparing two malware variants in each family using iBinHunt. Similarly, the column 5∼7 shows the effect to reduce the number of STP invocations. In summary, our approach outperforms conventional iBinHunt in terms of less symbolic execution time by a factor of 4.0x on average, and fewer STP invocations by 4.3x on average.

Optimizations Breakdown Table 3 presents our optimizations breakdown when performing lineage inference for the four large malware families shown in Fig. 3. The first row shows the ratio of matched basic block pairs with the same byte sequences after normalization (line 4 in Algorithm 2). The low ratio also demonstrates the necessity of semantics-based binary diffing approach. The next two rows list statistics of union-find set, including number of union-find subsets and the maximum number of equivalent basic blocks in one subset. The row 4 and 5 present the hit rate of union-find set (line 7 in Algorithm 2) and DiffMap (line 10 in Algorithm 2). The row 6 shows the time cost incurred by building and managing the union-find set structure and DiffMap. The following two rows lists hit rate and time cost for QueryMap. The saving of concretizing symbolic formulas is shown in row 9, in which we avoid at least more than 50% output variables comparisons. At last, we present the overall memory cost to maintain union-find set, DiffMap and QueryMap. Reassuringly, the overhead introduced by our optimizations is small.

Related Work

Our efforts attempt to speed up semantics-based binary diffing, which can find equivalent binary pairs that reveal syntactic differences [START_REF] Gao | BinHunt: Automatically finding semantic differences in binary programs[END_REF][START_REF] Luo | Semanticsbased obfuscation-resilient binary code similarity comparison with applications to software plagiarism detection[END_REF][START_REF] Ming | iBinHunt: Binary hunting with interprocedural control flow[END_REF][START_REF] Heng | Exposé: Discovering potential binary code reuse[END_REF]. We have introduced the latest work in this direction in Section 2. In this section, we focus on the literature related to our optimization approach. Malware normalization relies on ad-hoc rules to undo the obfuscations applied by malware developers [START_REF] Bruschi | Using code normalization for fighting self-mutating malware[END_REF][START_REF] Christodorescu | Malware normalization[END_REF]. Our approach first performs a simple normalization to eliminate the effect of memory relocation and instruction idioms. Yang et al. [START_REF] Yang | Memoized symbolic execution[END_REF] proposed Memoise, a trie-based data structure to cache the key elements of symbolic execution, so that successive forward symbolic execution can reuse previously computed results. Our union-find structure is like Memoise in that we both maintain an efficient tree-based data structure to avoid re-computation. However, our approach aims to accelerate basic blocks matching and our symbolic execution is limited in a basic block, which is a straight line code without path conditions. Our optimization of caching equivalence queries is inspired by both EXE [START_REF] Cadar | EXE:automatically generating inputs of death[END_REF] and KLEE [START_REF] Cadar | KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs[END_REF], which cache the result of path constraint solutions to avoid redundant constraint solver calling. Different from the complicated path conditions cached by EXE and KLEE, our equivalence queries are simple and compact. As a result, our QueryMap enjoys a higher cache hit rate.

Conclusion

The high performance penalty introduced by the state-of-the-art semanticsbased binary diffing approaches restricts their application from large scale application such as analyzing numerous malware samples. In this paper, we first studied the cruxes leading to the performance bottleneck and then proposed memoization optimization to speed up semantics-based binary diffing. The experiment on malware lineage inference demonstrated the efficacy of our optimizations with only minimal overhead. Another possible application of our approach is to study the life cycle of metamorphic malware variants. we plan to explore this direction in our future work.

Fig. 2 .

 2 Fig. 2. Output formulas equivalence query results

Fig. 5 .Algorithm 2

 52 Fig. 5. Example of MakeSet-Union-Find operations

Fig. 6 .

 6 Fig.6. The impact of basic blocks fast matching on malware lineage inference: O1 (normalization), O2 (O1 + union-find set and DiffMap), O3 (O2 + concretizing symbolic formulas), O4 (O3 + QueryMap).

Fig. 7 .

 7 Fig. 7. The effect of our optimizations over time on Sasser family

  Create an initial subset structure containing one element, which is represented by a basic block's MD5 value. Each element's parent points to itself and has 0 depth. 2. Find: Determine which subset a basic block belongs to. Find operation can be used to quickly find two basic blocks are equivalent if both of them are within the same subset. 3. Union: Unite two subsets into a new single subset. The depth of new set will be updated accordingly.

	Basic block 2 (obfuscated)
	lea eax, [ebx]
	mov edx, 0x000A nop nop add eax, edx xchg eax, eax xor ebx, ebx lea edx, [ebx] add ecx, ebx not ecx	Normalization	lea eax, [ebx] mov edx, 0x000A add eax, edx jmp 0x000000 xor ebx, ebx lea edx, [ebx] not ecx add ecx, ebx	MD5 value
	jmp 0x401A22
	Fig. 4. Basic block normalization
	1. MakeSet:

Table 1 .

 1 Dataset statistics

		True
	9:	end if
	10:	if DiffMap(Find(a ), Find(b ))=1 then	semantically different subsets
	11:	return False
	12:	else
	13:	Perform symbolic execution on a and b
	14:	Check semantical equivalence of a and b
	15:	if a ∼ b then	a , b are semantically equivalent
	16:	Union(a , b )
	17:	Update DiffMap
	18:	return True
	19:	else	a , b are not semantically equivalent
	20:	Set DiffMap(Find(a ), Find(b ))
	21:	return False
	22:	end if
	23:	end if
	24: end function

Table 3 .

 3 Optimization breakdown

		StartPage Delf Mimail Ping
	Normalization ratio	9%	12% 12% 51%
	# union-find subsets	125	130 304 546
	Max. # basic blocks in one subset	5	6	8	10
	union-find hit rate	36%	44% 37% 41%
	DiffMap hit rate	47%	53% 44% 54%
	Union-find set and DiffMap cost (s)	9.5	14.3 12.0 13.7
	QueryMap hit rate	62%	70% 65% 75%
	QueryMap cost (s)	8.6	8.8	6.4	7.6
	Concretizing saving	60%	65% 55% 52%
	Memory cost (MB)	10	12	28	45

Acknowledgements

This research is supported in part by the National Science Foundation (NSF) grants CCF-1320605 and CNS-1223710.