Jim E Newton
email: jnewton@lrde.epita.fr

Didier Verna
email: didier@lrde.epita.fr

Maximilien Colange
email: maximilien.colange@lrde.epita.fr

Programmatic Manipulation of Common Lisp Type Specifiers

Keywords: CCS Concepts, Theory of computation Ñ Data structures design and analysis, Type theory, •Computing methodologies Ñ Representation of Boolean functions, •Mathematics of computing Ñ Graph algorithms

In this article we contrast the use of the s-expression with the BDD (Binary Decision Diagram) as a data structure for programmatically manipulating Common Lisp type specifiers. The s-expression is the de facto standard surface syntax and also programmatic representation of the type specifier, but the BDD data structure offers advantages: most notably, type equivalence checks using s-expressions can be computationally intensive, whereas the type equivalence check using BDDs is a check for object identity. As an implementation and performance experiment, we define the notion of maximal disjoint type decomposition, and discuss implementations of algorithms to compute it: a brute force iteration, and as a tree reduction. The experimental implementations represent type specifiers by both aforementioned data structures, and we compare the performance observed in each approach.

INTRODUCTION

In this article we contrast two data structures used for programmatically manipulating Common Lisp type specifiers: the s-expression as described in the Common Lisp specification [4, Section 4.2.3], and the Binary Decision Diagram (BDD) [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF][START_REF] Akers | Binary decision diagrams[END_REF]. The homoiconic s-expression provides ease of manipulation, and in simple cases, a high degree of human readability. On the other hand BDDs offer interesting performance characteristics. BDDs are heavily used in electronic circuit generation, verification, model checking, and type system models such as in XDuce [START_REF] Hosoya | Regular expression types for XML[END_REF].

As an exposition implementation and performance exper-ELS '10 April 3-4, 2016, Brussels, Belgium Although MDTD is interesting in its own right, we do not attempt, in this paper, to motivate in detail the applications or implications of the problem. We consider such development and motivation a matter of future research. We present two approaches to compute the MDTD and separately implement the algorithms with both data structures, s-expressions and BDDs (4 implementations). Finally, we report performance characteristics of the four algorithms implemented in Common Lisp.

The remainder of this article proceeds as follows: Section 2 introduces the MDTD problem; Section 2.1 and Section 2.2 abstractly summarize two algorithms for solving the MDTD problem; Section 3 summarizes programmatic manipulation of Common Lisp type specifiers; Section 4 summarizes BDDs, implementation and optimization to work with the Common Lisp type system; Section 5 summarizes the s-expression and BDD approaches to the same problem; and Section 6 discusses the performance of the five algorithms. There is also a brief Section 7 of Conclusion and Future work.

DISJOINT TYPE DECOMPOSITION

We begin the discussion by presenting the problem of decomposing a set of overlapping types into non-overlapping subtypes. We first define precisely what we mean to calculate. Then in sections 2.1 and 2.2 we present two different algorithms for performing the calculation. Notation 1. We use the symbol, K, to indicate the disjoint relation between sets. I.e., we take A K B to mean A X B " H. We also say A M B to mean A X B ‰ H. Notation 2. We use the notation, A Ă B, (A Ą B) to indicate that A is either a strict subset (superset) of B or is equal to B. Definition 1. A disjoined set is a set of mutually disjoint subsets of a given U . Definition 2. Let U be a set and V be a set of subsets of U . The Boolean closure of V , denoted p V , is the (smallest) super-set of V such that α, β P p V ùñ tα X β, α X βu Ă p V .

We claim here without proof that there exists a unique Boolean closure of a given set of sets. A more complete discussion and formal proof are available [START_REF] Newton | Analysis of algorithms calculating the maximal disjoint decomposition of a set[END_REF].

Definition 3. Let U be a set and V be a finite set of non-empty subsets of U , V " tA1, A2, ..., AM u. The set D is said to be a disjoint decomposition of V , if D is disjoined, D Ă p V , and YD " YV .

Definition 4. If D is a disjoint decomposition of V which has more elements than any other disjoint decompositions of V , then D is said to be the maximal disjoint decomposition of V .

Again, we claim without proof that there exists a unique maximal disjoint decomposition of a given V . The problem statement: Given V " tA1, A2, ..., AM u, suppose that for each pair pAi, Ajq, we know which of the relations hold: Ai Ă Aj, Ai Ą Aj, Ai K Aj. We would like to compute the maximal disjoint decomposition of V . The Venn diagram in Figure 1 is an example for V " tA1, A2, ..., A8u. The maximal disjoint decomposition D " tX1, X2, ..., X13u of V is shown in Figure 2.

Disjoint Set Derived Expression

X1 A1 X A2 X A3 X A4 X A6 X A8 X2 A2 X A3 X A4 X3 A2 X A3 X A4 X4 A3 X A2 X A4 X5 A2 X A3 X A4 X6 A2 X A4 X A3 X7 A3 X A4 X A2 X8 A4 X A2 X A3 X A8 X9 A5 X10 A6 X11 A7 X12 A8 X A4 X13 A4 X A8 X A5
In Common Lisp, a type is a set of (potential) values [4, Section Type], so it makes sense to consider the maximal disjoint decomposition of a set of types.

Computing a disjoint decomposition when we are permitted to look into the sets has been referred to as union find [START_REF] Patwary | Experiments on union-find algorithms for the disjoint-set data structure[END_REF][START_REF] Galler | An improved equivalence algorithm[END_REF]. However, we wish to solve the problem without knowledge of the specific elements; i.e. we are not permitted to iterate over or visit the individual elements. The correspondence of types to sets and subtypes to subsets thereof is also treated extensively in the theory of semantic subtyping [START_REF] Castagna | A gentle introduction to semantic subtyping[END_REF].

The RTE Algorithm

The algorithm for calculating the maximal disjoint decomposition used in the Common Lisp package regular-typeexpressions 1 [14] is shown below. This algorithm is straightforward and brute force. A notable feature of this algorithm is that it easily fits in 40 lines of Common Lisp code, so it is easy to implement and easy to understand, albeit not the most efficient possible in terms of run-time performance.

1. Let U be the set of sets. Let V denote the set of disjoint sets, initially D " H.

2. Identify all the sets which are disjoint from each other and from all the other sets. (Opn 2 q search) Remove these sets from U and collect them in D.

3.

If there are no sets remaining in U , we are finished. D is the set of disjoint sets.

4.

Otherwise, find one pair of sets, X P U and Y P U , for which X X Y ‰ H.

5.

From X and Y derive at most three new sets X X Y , XzY , and Y zX, preforming logic reductions as necessary. There are three cases to consider:

(a) If X Ă Y , then X X Y " X

The graph based algorithm

One of the sources of inefficiency of the algorithm explained in Section 2.1 is at each iteration of the loop, an Opn 2 q search is made to find sets which are disjoint from all remaining sets. This search can be partially obviated if we employ a little extra book-keeping. The fact to realize is that if X K A and X K B, then we know a priori that X K A X B, X K AzB, X K BzA. This knowledge eliminates some of useless operations.

This algorithm is semantically very similar to the algorithm shown in Section 2.1, but rather than relying on Common Lisp primitives to make decisions about connectivity of types, it initializes a graph representing the initial relationships, and thereafter manipulates the graph maintaining connectivity information. This algorithm is more complicated in terms of lines of code, 250 lines of Common Lisp code as opposed to 40 lines for the algorithm in Section 2.1.

Figure 3 shows a graph representing the topology (connectedness) of the diagram shown in Figure 1. Nodes1 , 2 , ... 8 in Figure 3 correspond respective to A1, A2, ... A8 in Figure 1. Blue arrows correspond to subset relations, pointing from subset to superset, and green lines correspond to other non-disjoint relations.

To construct this graph first eliminate duplicate sets. I.e., if X Ă Y and X Ą Y , then discard either X or Y . It is necessary to consider each pair pX, Y q of sets, Opn 2 q loop.

' If X Ă Y , draw a blue arrow X Ñ Y ' Else if X Ą Y , draw a blue arrow X Ð Y ' Else if X M Y , draw green line between X and Y .
' If it cannot be determined whether X Ă Y , assume the worst case, that they are non-disjoint, and draw green line between X and Y .

This construction assures that no two nodes have both a green line and also a blue arrow between them.

The algorithm proceeds by breaking the green and blue connections, in explicit ways until all the nodes become isolated. There are two cases to consider. Repeat alternatively applying both tests until all the nodes become isolated.

Subset relation

A blue arrow from X to Y may be eliminated if X has no blue arrow pointing to it, in which case Y must be relabeled as Y X X as indicated in Figure 4.

Figure 4 illustrates this mutation. Node Y may have other connections, including blue arrows pointing to it or from it, and green lines connected to it. However node X has no blue arrows pointing to it; although it may have other blue arrows pointing away from it.

If X touches (via a green line) any sibling nodes, i.e. any other node that shares Y as super-class, then the blue arrow is converted to a green line. In the before image of Figure 4 there is a blue arrow from 3 to Y and in the after image this arrow has been converted to a green line.

Touching connections

A green line connecting X and Y may be eliminated if neither X nor Y has a blue arrow pointing to it. Consequently, X and Y must be relabeled and a new node must be added to the graph as indicated in Figure 5. The figure illustrates the step of breaking such a connection between nodes X and Y by introducing the node Z .

Construct blue arrows from this node, Z, to all the nodes which either X or Y points to (union). Construct green Before

5 0 Y 1 2 4 X 3
After lines from Z to all nodes which both X and Y connect to (intersection). If this process results in two nodes connected both by green and blue, omit the green line.

5 0 Y 1 2 4 X 3 Node Re-labeled Boolean expression X X Y Y X X

TYPE SPECIFIER MANIPULATION

To correctly implement the MDTD by either strategy described above, we need operators to test for type-equality, type disjoint-ness, subtype-ness, and type-emptiness. Given a subtype predicate, the other predicates can be constructed. The emptiness check:

A " H ðñ A Ă H. The dis- joint check: A K B ðñ A X B Ă H. Type equivalence A " B ðñ A Ă B and B Ă A.
Common Lisp has a flexible type calculus making type specifiers human readable and also related computation possible. Even with certain limitations, s-expressions are an intuitive data structure for programmatic manipulation of type specifiers in analyzing and reasoning about types.

If T1 and T2 are Common Lisp type specifiers, the type specifier (and T1 T2) designates the intersection of the types. Likewise (and T1 (not T2)) is the type difference. The empty type and the universal type are designated by nil and t respectively. The subtypep function serves as the subtype predicate. Consequently (subtypep '(and T1 T2) nil) computes whether T1 and T2 are disjoint.

There is an important caveat however. The subtypep function is not always able to determine whether the named types have a subtype relationship [START_REF] Baker | A decision procedure for Common Lisp's SUBTYPEP predicate[END_REF][START_REF] Newton | Report: Efficient dynamic type checking of heterogeneous sequences[END_REF]. In such a case, subtypep returns nil as its second value. This situation occurs most notably in the cases involving the satisfies type specifier. For example, to determine whether the (satisfies F) type is empty, it would be necessary to solve the halting problem, finding values for which the function F returns true.

As a simple example of how the Common Lisp programmer might manipulate s-expression based type specifiers, consider the following problem. In SBCL 1.3.0, the expres-Before As mentioned above, programs manipulating s-expression based type specifiers can easily compose type intersections, unions, and relative complements as part of reasoning algorithms. Consequently, the resulting programmatically computed type specifiers may become deeply nested, resulting in type specifiers which may be confusing in terms of human readability and debuggability. Consider the following programmatically generated type specifier.

0 X Y 3 1 2 4 After 0 X 3 Y 1 2 Z 4 Node Re-labeled Boolean expression X X X Y Y X X Y Z X X Y
( or ( or ( and ( and number ( not bignum ))

( not ( or fixnum ( or bit ( eql -1))))) ( and ( and ( and number ( not bignum ))

( not ( or fixnum ( or bit ( eql -1))))) ( not ( or fixnum ( or bit ( eql -1)))))) ( and ( and ( and number ( not bignum ))

( not ( or fixnum ( or bit ( eql -1))))) ( not ( or fixnum ( or bit ( eql -1))))))

This type specifier is perfectly reasonable for programmatic use, but confusing if it appears in an error message, or if the developer encounters it while debugging. This somewhat obfuscated type specifier is semantically equivalent to the more humanly readable form (and number (not bignum) (not fixnum)). Moreover, it is possible to write a Common Lisp function to simplify many complex type specifiers to simpler form.

There is a second reason apart from human readability which motivates reduction of type specifiers to canonical form. The problem arises when we wish to programmatically determine whether two s-expressions specify the same type, or in particular when a given type specifier specifies the nil type. Sometimes this question can be answered by calls to subtypep as in (and (subtypep T1 T2) (subtypep T2 T1)). However, as mentioned earlier, subtypep is allowed to return nil,nil in some situations, rendering this approach futile in many cases. If, on the other hand, two type specifiers can be reduced to the same canonical form, we can conclude that the specified types are equal.

We have implemented such a function, reduce-lisp-type. It does a good job of reducing the given type specifier toward a canonical form, by repeatedly recursively descending the expression, re-writing sub-expressions, incrementally moving the expression toward a fixed point. We choose to convert the expression to a disjunctive normal form, e.g.,

BINARY DECISION DIAGRAMS

A challenge using s-expressions for programmatic representation of type specifiers is the need to after-the-fact reduce complex type specifiers to a canonical form. This reduction can be computationally intense, and difficult to implement correctly. We present here a data structure called the Binary Decision Diagram (BDD) [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF][START_REF] Akers | Binary decision diagrams[END_REF], which obviates much of the need to reduce to canonical form because it maintains a canonical form by design. Before looking at how the BDD can be used to represent Common Lisp type specifiers, we first look at how BDDs are used traditionally to represent Boolean equations. Thereafter, we explain how this traditional treatment can be enhanced to represent Common Lisp types.

Representing Boolean expressions

Andersen [START_REF] Andersen | An introduction to binary decision diagrams[END_REF] summarized many of the algorithms for efficiently manipulating BDD. Not least important in Andersen's discussion is how to use a hash table and dedicated constructor function to eliminate redundancy within a single BDD and within an interrelated set of BDDs. The result of Andersen's approach is that if you attempt to construct two BDDs to represent two semantically equivalent but syntactically different Boolean expressions, then the two resulting BDDs are pointers to the same object. Figure 6 shows an example BDD illustrating a function of three Boolean variables: A1, A2, and A3. To reconstruct the

A1 A2 1 A3 1 0 A3 0 1 Figure 6: BDD for pA 1 ^A2 q_pA 1 ^ A 2 ^A3 q_p A 1 ^ A 3 q
DNF (disjunctive normal form), collect the paths from the root node, A1, to a leaf node of 1, ignoring paths terminated by 0. When the right child is traversed, the Boolean complement ( ) of the label on the node is collected (e.g. A3), and when the left child is traversed the non-inverted parent is collected. Interpret each path as a conjunctive clause, and form a disjunction of the conjunctive clauses. In the figure the three paths from A1 to 1 identify the three conjunctive clauses pA1 ^A2q, pA1 ^ A2 ^A3q, and p A1 ^ A3q.

Representing types

Castagna [START_REF] Castagna | Covariance and contravariance: a fresh look at an old issue[END_REF] explains the connection of BDDs to type theoretical calculations, and provides straightforward algorithms for implementing set operations (intersection, union, relative complement) of types using BDDs. The general recursive algorithms for computing the BDDs which represent the common Boolean algebra operators are straightforward.

Let B, B1, and B2 denote BDDs, B1 " pif a1 C1 D1q and B2 " pif a2 C2 D2q.

C1, C2, D1, and D2 represent BDDs. The a1 and a2 are intended to represent type names, but for the definition to work it is only necessary that they represent labels which are order-able. We would eventually like the labels to accommodate Common Lisp type type names, but this is not immediately possible.

The formulas for pB1 _ B2q, pB1 ^B2q, and pB1 z B2q are similar to each other. If ˝P t_, ^, zu, then

B 1 ˝B2 " $ ' & ' %
pif a 1 pC 1 ˝C2 q pD 1 ˝D2 qq for a 1 " a 2 pif a 1 pC 1 ˝B2 q pD 1 ˝B2 qq for a 1 ă a 2 pif a 2 pB 1 ˝C2 q pB 1 ˝D2 qq for a 1 ą a 2 There are several special cases, the first three of which serve as termination conditions for the recursive algorithms.

' pt _ Bq and pB _ tq reduce to t. ' pnil ^Bq, pB ^nilq, and pBztq reduce to nil. ' pt ^Bq, pB ^tq, pnil _ Bq, and pB _ nilq reduce to B.

' pt z pif a B1 B2qq reduces to pif a ptzB1q ptzB2qq.

Representing Common Lisp types

We have implemented the BDD data structure as a set of Clos classes. In particular, there is one leaf-level Clos class for an internal tree node, and one singleton class/instance for each of the two possible leaf nodes, true and false.

The label of the BDD contains a Common Lisp type name, and the logical combinators (and, or, and not) are represented implicitly in the structure of the BDD.

A disadvantage BDDs present when compared to s-expressions as presented in Section 3 is the loss of homoiconicity. Whereas, s-expression based type-specifiers may appear in-line in the Common Lisp code, BDDs may not.

A remarkable fact about this representation is that any two equivalent Boolean expressions have exactly the same BDD structural representation, provided the node labels are consistently totally ordered. For example the expression from Figure 6, pA1 ^A2q _ pA1 ^ A2 ^A3q _ p A1 ^ A3q is equivalent to pp A1 _ A2q^p A1 _A2 _ A3q ^pA1 _ A3qq. So they both have the same shape as shown in the Figure 6. However, if we naïvely substitute Common Lisp type names for Boolean variables in the BDD representation as suggested by Castagna, we find that this equivalence relation does not hold in many cases related to subtype relations in the Common Lisp type system.

An example is that the Common Lisp two types (and (not arithmetic-error) array (not base-string)) vs. (and array (not base-string)) are equivalent, but the naïvely constructed BDDs are different: In order to assure the minimum number of BDD allocations possible, and thus ensure that BDDs which represent equivalent types are actually represented by the same BDD, the suggestion by Andersen [START_REF] Andersen | An introduction to binary decision diagrams[END_REF] is to intercept the BDD constructor function. This constructor should assure that it never returns two BDD which are equal but not eq.

Canonicalization

Several checks are in place to reduce the total number of BDDs allocated, and to help assure that two equivalent Common Lisp types result in the same BDD. The following sections, 4.4.1 through 4.4.5 detail the operations which we found necessary to handle in the BDD construction function in order to assure that equivalent Common Lisp type specifiers result in identical BDDs. The first two come directly from Andersen's work. The remaining are our contribution, and are the cases we found necessary to implement in order to enhance BDDs to be compatible with the Common Lisp type system.

We have not yet formally proven that this list of enhancements is complete. There very well may be other exotic cases we have not covered, and we consider that opportunity for future work.

Equal right and left children

An optimization noted by Andersen is that if the left and right children are identical then simply return one of them, without allocating a new BDD [START_REF] Andersen | An introduction to binary decision diagrams[END_REF].

Caching BDDs

Another optimization noted by Andersen is that whenever a new BDD is allocated, an entry is made into a hash table so that the next time a request is made with the exactly same label, left child, and right child, the already allocated BDD is returned. We associate each new BDD with a unique integer, and create a hash key which is a list (a triple) of the type specifier (the label) followed by two integers corresponding to the left and right children. We use a Common Lisp equal hash table for this storage, although we'd like to investigate whether creating a more specific hash function specific to our key might be more efficient.

Reduction in the presence of subtypes

Since the nodes of the BDD represent Common Lisp types, other specific optimizations are made. The cases include situations where types are related to each other in certain ways: subtype, supertype, and disjoint types. In particular there are 12 optimization cases, detailed in Table 1. Each of these optimizations follows a similar pattern: when constructing a BDD with label X, search in either the left or right child to find a BDD, Case Child to search Relation Reduction

1 X.lef t X K Y Y Ñ Y.right 2 X.lef t X K Y Y Ñ Y.lef t 3 X.right X K Y Y Ñ Y.right 4 X.right X K Y Y Ñ Y.lef t 5 X.right X Ą Y Y Ñ Y.right 6 X.right X Ą Y Y Ñ Y.lef t 7 X.lef t X Ą Y Y Ñ Y.right 8 X.lef t X Ą Y Y Ñ Y.lef t 9 X.lef t X Ă Y Y Ñ Y.lef t 10 X.lef t X Ă Y Y Ñ Y.right 11 X.right X Ă Y Y Ñ Y.lef t 12 X.right X Ă Y Y Ñ Y.right

Reduction to child

The list of reductions described in Section 4.4.3 fails to apply in cases where the root node itself needs to be eliminated. For example, since vector Ă array we would like the following reductions: .

The solution which we have implemented is that before constructing a new BDD, we first ask whether the resulting BDD is type-equivalent to either the left or right children using the subtypep function. If so, we simply return the appropriate child without allocating the parent BDD. The expensive of this type-equivalence is mitigated by the memoization. Thereafter, the result is in the hash table, and it will be discovered as discussed in Section 4.4.2.

More complex type relations

There are a few more cases which are not covered by the above optimizations. Consider the following BDD: This represents the type (and (not integer) (not ratio) rational), but in Common Lisp rational is identical to (or integer ratio), which means (and (not integer) (not ratio) rational) is the empty type. For this reason, as a last resort before allocating a new BDD, we check, using the Common Lisp function subtypep, whether the type specifier specifies the nil or t type. Again this check is expensive, but the expense is mitigated in that the result is cached.

MDTD IN COMMON LISP

When attempting to implement the algorithms discussed in Sections 2.1 and 2.2 the developer finds it necessary to choose a data structure to represent type specifiers. Which ever data structure is chosen, the program must calculate type intersections, unions, and relative complements and type equivalence checks and checks for the empty type. As discussed in Section 3, s-expressions (i.e. lists and symbols) is a valid choice of data structure and the aforementioned operations may be implemented as list constructions and calls to the subtypep predicate. As introduced in Section 4, another choice of data structure is the BDD. Using the BDD data structure along with the algorithms described in Section 4 we can efficiently represent and manipulate Common Lisp type specifiers. We may programmatically represent Common Lisp types largely independent of the actual type specifier representation. For example the following two type specifiers denote the same set of values: (or number (and array (not vector))) and (not (and (not number) (or (not array) vector))), and are both represented by the BDD shown in Figure 5. Moreover, unions, intersections, and relative complements of Common Lisp type specifiers can be calculated using the reduction BDD manipulation rules also explained in Section 4.

We have made comparisons of the two algorithms described in Sections 2.1, 2.2. One implementation of each uses s-expressions, one implementation of each uses BDDs. Some results of the analysis can be seen in Section 6.

Using BDDs in these algorithm allows certain checks to be made more easily than with the s-expression approach. For example, two types are equal if they are the same object (pointer comparison, eq). A type is empty if it is identically the empty type (pointer comparison). Finally, given two types (represented by BDDs), the subtype check can be made using the following function:

( defun bdd-subtypep ( bdd-sub bdd-super ) ( eq * bdd-false * ( bdd-and-not bdd-sub bdd-super )))

This implementation of bdd-subtype should not be interpreted to mean that we have obviated the need for the Common Lisp subtypep function. In fact, subtypep, is still useful in constructing the BDD itself. However, once the BDDs have been constructed, and cached, subtype checks may at that point avoid calls to subtypep, which in some cases might otherwise be more compute intensive.

PERFORMANCE OF MDTD

Sections 2.1 and 2.2 explained two different algorithms for calculating type decomposition. We look here at some performance characteristics of the two algorithms. The algorithms from Section 2.1 and Section 2.2 were tested using both the Common Lisp type specifier s-expression as data structure and also using the BDD data structure as described in Section 5. Figures 9 and8 contrast the four effective algorithms in terms of execution time vs sample size.

We attempted to plot the results many different ways: time as a function of input size, number of disjoint sets in the input, number of new types generated in the output. Some of these plots are available in the technical report [START_REF] Newton | Analysis of algorithms calculating the maximal disjoint decomposition of a set[END_REF]. The plot which we found heuristically to show the strongest visual correlation was calculation time vs the integer product of the number of given input types multiplied by the number of calculated output types. E.g., if the algorithm takes a list of 5 type specifiers and computes 3 disjoint types in 0.1 seconds, the graph contains a point at (15,0.1). Although we don't claim to completely understand why this particular plotting strategy shows better correlation than the others we tried, it does seem that all the algorithms begin a Opn 2 q loop by iterating over the given set of which is incrementally converted to the output types, so the algorithms in some sense finish by iterating over the output types. More research is needed to better understand the correlation.

Performance Test Setup

The type specifiers used in Figure 9 are those designating all the subtypes of number. The type specifiers used in Figure 8 are those designating a randomly selected set of types specified in Figure 4-2 The performance tests including starting with a list of randomly selected type specifiers from a pool, calling each of the four functions to calculate the disjoint decomposition, and recording the time of that calculation. We have plotted in Figures 8 and9 the results of the runs which took less than 30 seconds to complete. This omission does not in any way effect the presentation of which algorithms were the fastest on each test. The tests were performed on a MacBook 2 GHz Intel Core i7 processor with 16GB 1600 MHz DDR3 memory, and using SBCL 1.3.0 ANSI Common Lisp.

Analysis of Performance Tests

There is no clear winner. Some of the algorithms do better in some tests and worse in other tests. It seems the tree based algorithms do very well. Often the better of these two algorithms is the BDD based one as shown in Figure 8. However there is a notable exception shown in Figures 9 where graph algorithm using s-expressions performs best.

CONCLUSION AND FUTURE WORK

We believe our contribution in this paper includes, introducing the BDD as an alternative to the s-expression in programmatic manipulation of Common Lisp type specifiers, extending the BDD definition to accomodate a type system which regards subtypes as subsets. Our contribution also includes an efficient graph based algorithm for calculating the maximal disjoint type decomposition.

The MDTD problem is potentially interesting in its own right. Although, we do not attempt, in this paper, to motivate in detail the applications or implications of the problem, we suspect there may be a connection between the problem, and efficient compilation of type-case and its use in improving pattern matching capabilities of Common Lisp. We consider such development and motivation a matter of future research.

An immediate priority in our research is to formally prove the correctness of our algorithms, most notably the graph decomposition algorithm from Section 2.2. Experimentation leads us to believe that the graph algorithm always terminates with the correct answer, nevertheless we admit there may be exotic cases which cause deadlock or other errors.

As far as the performance analysis is concerned, it is not yet understood why we see drastically different performance It is known that algorithms using BDD data structure tend to trade space for speed. Castagna [START_REF] Castagna | Covariance and contravariance: a fresh look at an old issue[END_REF] suggests a lazy version of the BDD data structure which may reduce the memory footprint, which would have a positive effect on the BDD based algorithms.

We have spent only a few weeks optimizing our BDD implementation based on the Andersen's description [START_REF] Andersen | An introduction to binary decision diagrams[END_REF], whereas the CUDD [START_REF] Somenzi | CUDD: BDD package[END_REF] developers have spent many years of research optimizing their algorithms. Certainly our BDD algorithm can be made more efficient using techniques of CUDD or others. It has also been observed that in the algorithm explained in section 2.2 that the convergence rate varies substantially depending on the order the reduction operations are performed. We do not yet have enough data to characterize this dependence. Furthermore, the order to break connections in the algorithm in Section 2.2. It is clear that many different strategies are possible, (1) break busiest connections first, (2) break connections with the fewest dependencies, (3) random order, (4) closest to top of tree, etc. These are all areas of ongoing research.

We plan to investigate whether there are other applications MDTD outside the Common Lisp type system. We hope the user of Castagna's techniques [START_REF] Castagna | Covariance and contravariance: a fresh look at an old issue[END_REF] on type systems with semantic subtyping may benefit from the optimizations we have discussed.

A potential application with Common Lisp is improving the subtypep implementation itself, which is known to be slow in some cases. Section 5 gave a BDD specific implementation of bdd-subtypep. We intend to investigate whether existing Common Lisp implementations could use out technique to represent type specifiers in their inferencing engines, and thereby make some subtype checks more efficient.

Figure 1 :

 1 Figure 1: Example Venn Diagram

Figure 2 :

 2 Figure 2: Disjoint Decomposition of Sets from Figure 1

Figure 3 :

 3 Figure 3: Topology graph

Figure 4 :

 4 Figure 4: Subset before and after mutation

Figure 5 :

 5 Figure 5: Touching connections before and after mutation

  (or (and (not a) b) (and a b (not c))). The reduction procedure follows the models presented by Sussman and Abelson [1, p. 108] and Norvig [15, ch. 8].

.

  If X and Y have a particular relation, different for each of the 12 cases, then the Y L R BDD reduces either to L or R. Two cases, 5 and 7, are further illustrated below.

Case 7 :

 7 If X Ą Y and Y L R appears in X.lef t, then Y L R reduces to R. E.g., integer Ă string; if X " string and Y " integer; thus

Figure 7 :

 7 Figure 7: BDD representing (or number (and array (not vector))

(

  arithmetic-err o r function ( and arithmet i c -e r r o r function ) ( or arithmeti c -e r r or function ) array ( or function array ) sequence ( or function sequence )) ...)

Figure 8 :

 8 Figure 8: Combinational CL types

Figure 9 :

 9 Figure 9: Subtypes of number

  and XzY " H. Thus update U by removing Y , and adding Y zX.

	(b) If Y Ă X, then X X Y " Y and Y zX " H. Thus
	update U by removing X, and adding XzY .
	(c) Otherwise, update U by removing X and Y , and
	adding X X Y , XzY , and Y zX.
	6. Repeat steps 2 through 5 until U " H, at which point
	we have collected all the disjoint sets in D.

Table 1 : BDD optimizations Case

 1

5: If X Ą Y and Y L R appears in X.right, then Y L R reduces to R. E.g., integer Ă number; if X " number and Y " integer; thus

. Standardized Atomic Type Specifiers from

  the Common Lisp specification [4, Section 4.2.3 Type Specifiers] lists the names of 97 types which every compliant Common Lisp implementation must support. Starting from this list, we randomly generated type specifiers using and and or combinations of names from this list such as the following:

https://gitlab.lrde.epita.fr/jnewton/regular-typeexpression, The Common Lisp package source code is available from the EPITA/LRDE website.


Leonardo Regano
email: leonardo.regano@polito.it

Daniele Canavese
email: daniele.canavese@polito.it

Cataldo Basile
email: cataldo.basile@polito.it

Alessio Viticchié
email: alessio.viticchie@polito.it

Antonio Lioy
email: lioy@polito.it

Towards Automatic Risk Analysis and Mitigation of Software Applications

Keywords: software protection, software risk analysis, software attacks

This paper proposes a novel semi-automatic risk analysis approach that not only identifies the threats against the assets in a software application, but it is also able to quantify their risks and to suggests the software protections to mitigate them. Built on a formal model of the software, attacks, protections and their relationships, our implementation has shown promising performance on real world applications. This work represents a first step towards a user-friendly expert system for the protection of software applications.

Introduction

Software is pervasive in our life. We rely on software applications for our leisure and to ease our work, regardless of our fields of activity. In addition, software is one of the pillars of the world economy that moves billions to trillions of dollars. Developers have to protect their applications from tampering and avoid that confidential data in their software are disclosed. In short, companies have to protect the assets in their software, assets that are exposed to very powerful attacks, known as Man-at-the-End (MatE) attacks, from crackers that fully control the execution environment of the software to protect.

When the software must be protected, the human experience is the leading factor and almost the only one. While big companies have ad hoc teams to decide how to protect their applications or they can pay specialized companies, small and medium enterprises cannot afford the costs for properly protecting their software. By remaining vulnerable, it can damage the companies themselves, generating monetary losses, and all of us, becoming a vector for various kind of malware. Automatic or assisted techniques are needed to help software developers in protecting their applications.

In this paper we propose a novel risk analysis approach to (1) identify the threats against the assets in target applications, [START_REF] Shields | Anti-debugging -a developers view[END_REF] quantify their risks against them and (3) suggest potential mitigations. In this context, the mitigations are the protections applied to each asset in order to reduce their exposure to the identified risks. This work represents a first step towards an expert system that can drive the software developers in all the delicate phases of software protection. While the ambition is to make software protection another standard, almost push-button activity like the compilation, in the short term, our approach can be an interesting solution for small and medium enterprises.

A preliminary version of this work has been already published [START_REF] Basile | Automatic discovery of software attacks via backward reasoning[END_REF], focusing only on the automatic threats identification. With respect to our previous approach, the main improvements in this paper are the risk quantification and the proposal of mitigations. In addition, we greatly improved the expressivity of our model, thus leading to an increased accuracy of the attacks identification phase. A formal modelling of attacker purposes, strategies, and approaches to tampering, allows a more sophisticated analysis that also associates discovered attacks to the protections that would reduce their likelihood and consequences. Together with the formalization of a more sophisticated vulnerability identification system, building and validating our novel risk analysis model has required the impact's assessment of both attacks and protections on the software assets. For a better validation of our model, we have collected assessment information by means of questionnaires proposed to experts in software protection.

This paper is structured as follows. Section 2 presents our approach, its inputs, outputs and work-flow. Section 3 introduces a reference application that we will use to practically describe our achievements. Section 4 describes our formal model for describing an application for risk analysis purposes. Section 5 introduces the threats and mitigation identification engines whose performance is detailed in Section 6. Section 7 presents previous works in the field. Finally, Section 8 draws conclusions and sketches future research directions.

Approach

This section presents a general overview of our approach, whose work-flow is sketched in Fig. 1. The input to our system is the set of the source files of the application to protect. Currently, only the C and C++ languages are supported, but the same core ideas can be easily extended to any other programming language. The first phase, application model build, consists of a static analysis of the source code, which is parsed and analyzed to create an abstract model of the application. We named application part a generic piece of code of the application under analysis. The application parts are either data, that include (global and local) variables, class fields and function/method parameters, and code areas, which consist of functions, methods, classes or a particular code region in a function/method. Code areas have a hierarchical structure that allow them to contain other application parts. For instance, a class (a code area) can contain a method (another code area) that, in turn, encloses a local variable (a datum). Apart the containment association, application parts are also linked together via a set of other relationships, such as the call graph information. More information about these relationships is available in Section 4.

Once the initial application model has been automatically constructed, the user must finalize it by selecting which application parts actually need to be protected and the security properties that need to be guaranteed on them. Application parts that are associated to at least one security property are named assets. This is performed during the assets' identification phase. Identifying assets is pivotal in our approach as they are both the elements to protect (developers' perspective) and the targets of the attacks (attackers' perspective). We focus on four security properties in this work: integrity and confidentiality, which were already modelled in our previous paper, execution correctness and weak confidentiality, which are novel contributions.

For instance, some application parts can be marked with the integrity property, when they must be preserved from modifications. In this case, either the parts must be hard to modify or any modification must be detected. In other cases, the developers may want to guarantee the execution correctness, a stronger form of integrity that in addition requires that a code area must be called as expected. For instance, application parts marked with the execution correctness cannot be skipped, like authentication/license checks. Parts marked with the confidentiality property must be unintelligible for an attacker, such as keys to decrypt media streams or patented algorithms. Some data may be also tagged with the weak confidentiality property. This property is breached when the attacker is able to retrieve the datum at every moment of the application execution (thus for hard-coded data the weak confidentiality is the same as the normal confidentiality). This is mostly interesting for attacks that target the assets of a victim's application (i.e., not the attacker's copy) by means of a distributed approach aiming at continuously obtaining the data values. For instance, in case of an OTP (One-Time Password) generator 1 that generates the next password by hashing the value of a fixed seed and a counter modified at each generation, the variable storing the counter can be marked with weak confidentiality. To predict the next passwords (not only the next one), it does not suffice that the attacker obtains once the value of victim's counter, he has to obtain it just before every generation. Therefore, either he is able to access every time the victim's appli-cation to read the counter value, or he has to obtain one counter, understand the counter update function, and reproduce it on his copy.

During the assets' identification, the user is also given the opportunity to override the relationships that were previously automatically deduced or refine them with more precise associations. In addition, some important information may not be extracted by means of automatic tools as its correct identification would require knowledge that is not inferrable from the source code. For instance, correctly deducing that a function encrypts or decrypts some data is complex, especially if the code makes use of ad-hoc cryptographic libraries. Furthermore, some inferred relationships can be transformed into more accurate ones by means of a manual user intervention. As an example, a license verification function can invoke another function if and only if a previous license check is passed. These functions are automatically related by the automatic analysis with a simple call relationship. However our model supports a more expressive association, the enables one, used to indicate that a function can be only executed if another one has been "successfully" executed. To simplify this phase, we developed a simple yet effective domain specific language presented in Section 4. With this language, manually added data can be saved on disk, avoiding to ask the users to input them again at each analysis.

Once a valid and accurate application model has been constructed and validated by the user, during the vulnerability analysis phase, our system identifies all the attacks that can disrupt the security properties of the assets and produce a vulnerability report for the user. Attacks are sequences of simpler actions that an attacker must perform to mount it, the attack steps. Therefore, in our case, an attack is an ordered list of attack steps and will be thus called attack path. This simplification does not influence the accuracy of our analysis since we are interested in the effects of the attacks, regardless of their steps' order. For instance, two attack paths (step 1 , step 2 , step 3 ) and (step 1 , step 3 , step 2 ) are produced when both step 2 and step 3 can be executed at the same time or when their relative ordering does not matter. When producing the report to the user our approach will present only one of the two previous attack paths, by eliminating the clones. These sample attack paths are known as unique attack paths.

After having detected the attack paths, the strategy identification phase is performed. This phase consists in the classification of all the attack steps of the inferred attack paths in order to understand their purpose towards the goal. In our work, we classify attack steps in seven strategy types: static and dynamic code analysis, static and dynamic tampering, sniffing and spoofing, and compromission attacks. Note that, sniffing and spoofing also consider traditional network Man-in-the-Middle (MitM) attack steps while the compromission type includes code injection and attempts to control the application victim's copy2 .

Finally, the mitigation phase produces a mitigation report that lists all the protection techniques that can be used to mitigate (either block or render more difficult) all the attack paths. A protection, in our approach, is able to mitigate a set of attack step types with a particular level of efficacy (low, medium or high). We assume that an attack path is mitigated by a protection if it is able to mitigate at least one of its steps. This phase considers the following protections:

anti-debugging, which makes more difficult to perform dynamic analysis by attaching a trusted debugger, preventing attackers from using their own [START_REF] Shields | Anti-debugging -a developers view[END_REF]; -algorithm hiding, a set of obfuscation techniques against the reverse engineering, protecting a code's confidentiality and understandability [START_REF] Anckaert | Program obfuscation: a quantitative approach[END_REF]; -call stack checks, which verifies the execution correctness by checking that functions are called in the right order [START_REF] De Sutter | D2.08[END_REF]; -barrier slicing, which enforces the integrity of data and code areas by moving them to a trusted server where they will be executed [START_REF] Ceccato | Barrier slicing for remote software trusting[END_REF]; -code guards, which are checks added in an application to detect and react to integrity breaches [START_REF] Chang | Protecting software code by guard[END_REF]; -code mobility, which protects application parts from reverse engineering and analysis by removing them from the application to be installed at run time when they need to be executed [START_REF] Falcarin | Exploiting code mobility for dynamic binary obfuscation[END_REF]; -data hiding, which involves altering the data structures and the functions' data flow for ensuring data confidentiality [START_REF] Collberg | A taxonomy of obfuscating transformation[END_REF]; -remote attestation, which protects application integrity by forcing the application to periodically send integrity proofs to a verification server [START_REF] Coker | Principles of remote attestation[END_REF].

After having revised the protection proposed by the mitigation report, the suggested protections can be applied on the assets. This stage has been implemented within the ASPIRE project by tagging all the variables and code areas with some special annotations that are later processed by the custom ASPIRE protection tool-chain.

Reference Example

We introduce here one of the applications we used to test our approach, the Linux Memory Game 3 , an open source video game written in C based on the popular card game Memory. The game is played with a set of cards' pairs placed face down on a table. The player's goal is to find all the matching pairs with the minimum number of card turns. The game provides five skill levels: little one, beginner, skilled, master and daemon. When playing at the little one difficulty, all the cards are face up and visible (it is for children). On the other hand, in the highest difficulty level the cards are moved in different (and increasingly difficult) ways after every flip.

the cases where the attackers inject code to remotely control a pool of victims' applications. 3 The source code is available at https://packages.debian.org/stretch/lmemory. In our reference example, the main goal of the attacker is to win with the lowest number of flipped cards. On the other hand, the software developer must preserve the correctness of the game and the validity of the best scores, e.g., to keep the interest on it, as it happened for World of Warcraft.

Fig. 2 depicts a diagram showing the relationships (function calls, accesses and initializations of variables) between the most important application parts in the game. The card values are stored in the global variable lmem_state, a vector of integers whose elements are the cells in the card matrix, an asset. Its weak confidentiality must be safeguarded, as the attacker can play with all the cards visible, but also its integrity, since he can force a known card arrangement.

lmem_state is set by the lmem_Newgame() function, executed when a new game starts. lmem_Newgame() is also an asset, whose integrity must be preserved.

A critical datum is also click_count, an integer variable that counts the number of cards flipped. The developer must guarantee its integrity to avoid unwanted modifications (as an attacker can lower it to increase its final score).

The function lmem_flip_card() is executed every time a card is flipped and its logic can be summarized in the following steps: [START_REF] Basile | Automatic discovery of software attacks via backward reasoning[END_REF] when the user has clicked on a new card, turn its face up; (2) increase the click count; (3) if there are already two cards face up, then turn them face down; (4) if there is already a card face up and it matches with new card, remove both cards from the table ;  (5) rearrange all the face down cards according to the selected skill level.

The lmem_from_Little_One() function flips back all the cards and it is invoked by the lmem_Level() function, which in turn is called when the user changes the difficulty level from the little one level to a higher one. These three functions must be preserved from modifications since a plethora of attacks can be mounted against them, that is, their execution correctness must be guaranteed.

In the following sections, we will identify a set of attacks that can be used to alter the normal work-flow of the application. We will start our discussion by informally introduce some of them here.

The attacker might start by trying to discover the position of all the cards, even if they are face down, or to force a known card configuration. An attacker can locate lmem_state by debugging a function that writes this vector, such as lmem_Newgame(), executed when a new game starts, thus easily recognizable via dynamic or static analysis. He can force some card values in lmem_Newgame() by using a known card configuration from a previously played game.

The attacker can also statically or dynamically change lmem_Level() to avoid the invocation of lmem_from_Little_One(). In this way the attacker can start with the little one difficulty level then switch to a higher one to be able to play with all the card faced up.

Finally, every step of lmem_flip_card() is vulnerable. The attacker can tamper the code to avoid the click count increase in order to obtain a reasonable score (step 2). He can stop cards from being turned face down (step 3). He can skip the card matching check, thus all the pairs of cards will be removed from the table, allowing an easy victory (step 4). Finally, he can also pretend to play at a higher skill level, whilst having a game at a lower difficulty (step 5).

Application Modeling

Our approach aims at automatically inferring attacks and protections that mitigate them by means of a Knowledge Base (KB). In this context, the starting knowledge is the application itself. The application code is theoretically the best source of information, since it models the complete application behavior. However, it also contains low level details that are not interesting for our kind of analysis. Therefore, a more abstract form is better suited for our purposes, that is the application meta-model. In our meta-model, an application is essentially a container of several application parts that can be either a datum or a code area. A code area can recursively contain one or more other application parts.

Every application part has a name (e.g., the variable or function name) and a weight, a non-negative real number used to explicitly indicate its importance (the greater the weight the more important the part). Weights are only meaningful for the assets and are used to compute the risk values during the risk assessment phases. Application parts are associated to a non-empty list of security properties to ensure, which are also considered as the targets of the attacker.

The Data class stores an additional type attribute stating their data type (e.g., integer or string). This field is used to discard the unsuitable protections since some techniques might be applicable only to some kind of instances (e.g., data obfuscation for integer variables only).

Code areas are complex types with the following relationships:

a code area accesses a datum when it reads or writes its content; -a code area initializes a datum with a value (it represents the first writing of a value in a variable); -a code area calls another code area; -a code area enables another area if its execution depends on the (successful) execution of another area.

Our meta-model is simple and could be constructed by hand, but this task can be very time consuming as real applications might have hundreds or thousands of application parts. For this reason, the application model build phase in our approach automatically extract the application model from its source code and instantiates its components accordingly. As anticipated in Section 2, static analysis can lead to inaccurate or incomplete results that need to be complemented by the user input for validation and refinement purposes. To help users store this additional information, we developed a Domain Specific Language, the Application Description Language (ADL), which expresses the same concepts as the application meta-model, but in a more human readable form. Its Backus-Naur syntax rules are shown in Figure 4. ("properties" SecurityProperty ("," SecurityProperty )* "weight" FLOAT)? "}" | ";"); CodeArea ::= "codeArea" ID (("{" ("properties" SecurityProperty ("," SecurityProperty )* "weight" FLOAT)? (Relation ID ("," ID)*)* "}" ) | ";"); Relation ::= "accesses" | "initializes" | "calls" | "enables"; DatumType ::= "integer" | "integerArray" | ...; SecurityProperty ::= "confidentiality" | "weakConfidentiality" | "integrity" | "executionCorrectness"; The terminal symbols ID and FLOAT respectively represents a valid C/C++ identifier and a sign-less floating point value.

As an example, Fig. 5 reports the description in ADL of the lmem_flip_card(), lmem_Newgame() and lmem_state assets for the Memory game.

Vulnerability Analysis and Mitigation

In this section we present the vulnerability analysis and mitigation reporting steps of our approach. A preliminary work of the vulnerability analysis is available in a previously published paper [START_REF] Basile | Automatic discovery of software attacks via backward reasoning[END_REF], whose main ideas are summarized below:

-Facts are stored into a Knowledge Base (KB), initially populated with information concerning the application obtained from the application model. -Breaching the assets properties becomes the goal of the attackers. Goals are modelled as properties. In this paper, the properties are: confidentiality, weak confidentiality, integrity and execution correctness. -Attack step are modelled as rules of inference P → C (id), where id is an identifier of the attack step, that is its name, P is a set of premises, that is a set of facts in the KB that must be true in order to trigger the step, C is a set of conclusions, that is a set of additional facts that hold after the attack step is performed. Note that some attack steps (e.g. setting up a remote server) do not breach any security property, they are just preliminary actions needed to breach some properties (like the confidentiality of some data). -Some inferences are not attack steps, relating different steps/facts and application parts (i.e., if x is in the KB do not perform the attack step y).

Once the Knowledge Base has been populated, all the attack paths are obtained by means of backward programming, which starts from the attack steps that breach the goals and progressively adduces facts that make the premises of attack steps true until the axioms are reached (i.e., attack steps or facts that have no premises). Attack paths can be extracted in an automatic way with any inferential engine of choice.

The previous attack path discovery model has been improved by adding new inference types that allow the detection of a larger set of attacks. The most important improvement consists in making the model more expressive by introducing the concept of attack strategy. Strategies are formal ways to determine the behavior of an attacker and they are modelled by changing the way the backward reasoning process work. In some cases, strategies enable a different set of attack steps. For instance, if the attacker has to tamper with the victim's copy, he has to perform several network-oriented attack steps (e.g. creating fake servers, tampering with the victim's OS, injecting malware). More strategies can be enabled at the same time. Moreover, certain facts are derived only if certain attack strategies are applied and certain premises are enabled or disabled based on the strategy. Enabling more sophisticated strategies (that may include more attack steps and render premises more sophisticated require) may have a significant impact on the performance.

As a first instance of strategy, together with MatE attacks, we have modeled attack strategies depicting distributed scenarios, where an attacker tries to gain access to data of an application running on a victim PC. As an example, we have introduced an attack step modeling a code injection attack, where the attacker modifies a code of the victim application to send to him all the data accessed by the code. We also added strategies to breach the weak confidentiality. As anticipated, to breach this property, the attacker must know the value of the datum on the victim application at every moment of the application execution. In our internal model, we modelled additional preconditions: the attacker must not only obtain the value of the datum (e.g., with the code injection attack step described before), but he must also retrieve, either with static or dynamic attacks, all the code areas that access (and therefore potentially modify) the datum. Referring to the example application in Section 3, we have marked lmem_state, which contains the position of the cards, with the weak confidentiality. To breach it, the attacker must not only locate the datum in memory, but he must also execute the lmem_Newgame code before reading the datum value, because, as we can see in Fig. 2, lmem_Newgame initializes lmem_state. We also take into account the call graph of the application, thanks to the calls relationships: in particular, if a code has been executed, i.e., if the execute code step is present in the attack path, all the codes called by the first one are considered as executed.

We can also model indirect attack strategies, when the attacker has to start tampering with other parts of the application to achieve his goal. For instance, some code areas are executed only if first enabled by the execution of other code areas. An example may be an application that contains a license check function that, if performed successfully, enables the execution of the rest of the application. In our internal model a code area is enabled not only if the enabler code area has been executed before, but also if it have been changed, covering cases such as the license check in which the attacker, instead of using a working license, modifies the license check code to bypass it.

Another strategy has been defined to represent attacks against the execution correctness: an attacker can breach the execution correctness of a code not only modifying the latter, but also avoiding all the calls to it.

Finally, we greatly improved the accuracy of the attack path inference rules, which now leverage a greater number of relationships between the application parts, such as the ones described in Section 4. Furthermore, we added several new kind of attack steps, such as a new one representing the execution of a single code area, needed to better handle the relationships such as the initializes association and the dynamic attacks in general.

As as example, the attack where the attacker can play at higher level of difficulty with open cards by avoiding the call by lmem_Level() to lmem_from_Little_One (Section 3) can be automatically obtained by the attack deduction phase if lmem_from_Little_One is marked with the execution correctness property. In this case if the corresponding strategy is enabled it produces the different attack steps in Fig. 6. Attack paths are represented as rectangles, while attack facts are drawn with rounded rectangles. Links between attack steps are represented as thick arrows, while links between attack steps and the produced facts are draw with normal arrows. Facts deduced by other facts are linked with dashed arrows.

To help security engineers to select the most vulnerable assets and properly decide what to protect in their applications, we also provide a measure about how dangerous is an attack path. Of course, custom formulas can be used in alternative to adapt to target applications and their business models.

Given all the deduced attack paths AP i , all their attack steps AS i,j , and all the assets a k , we define the risk Ω ǫ APi of an attack path AP i against attackers with expertise ǫ as:

Ω ǫ APi = π(AP i , ǫ) Γ AP i (1)
Γ APi is a quantitative measure of the damage resulting from a successful attack path, calculated as the sum of the damage Γ AS i,j from each attack step:

Γ AP i = j Γ AS i,j = j k (W a k b(a k , AS i,j ))
where W a k is the user-defined asset weight, and b(a k , AS j ) is a function, deduced by our inference system, that returns the fraction of the security properties of the asset a k that are breached by the attack step AS j , that is, it returns 1 if all the security properties are compromised and 0 if none 4 . Finally, the values obtained with the risk formulas are mapped on a three values score (low, medium, high) with an ad hoc mapping.

Our inference system also suggests a list of protections that can be implemented to mitigate the risk of an attack. Protections can be applied to code areas and data, and are associated to a mitigation level, which is a measure of how much they reduce the probability of success of a particular attack step. To assess the mitigation of the risk associated to an attack path against application assets after the application of a set of protections selected by the user from the proposed ones, we recalculate the risk by using an updated value of the probability to successfully perform every attack step in the presence of the selected protections. To this purpose, we override the function π(AS i,j , ǫ) into π(AS i,j , ǫ, {p l } l ) that also considers that {p l } l protections are deployed to protect the asset.

The values of the expertise levels needed by the attacker to undertake an attack step, and the mitigation levels of the protections (and corresponding probabilities) that we have used in our experiments have been obtained by means of questionnaires proposed to 20 software protection experts in the ASPIRE project (https://aspire-fp7.eu/) consortium and advisory board.

Experimental Results

We have implemented our approach in Java 8 as a set of plug-ins for the Eclipse Mars platform. In addition we used XText 2.9.0 for developing the ADL parser and SWI-Prolog 7.2.3 for the attack path engine. In order to speed up the computation, the inference engine is implemented as a multi-threaded Prolog program so that multiple assets can be evaluated in parallel.

We tested our framework on the Linux Memory Game application described in Section 3. It is written in C and contains 53 application parts (10 global variables and 43 functions). We have marked 6 application parts as assets. The tests have been performed on an Intel i7-4980HQ 2.80 GHz with 16 GB of memory under Linux Debian 4.5.0, allocating 4 CPU cores for the vulnerability analysis phase. The whole analysis process completed in 344.1 seconds (less than 6 minutes) with all the attack strategies enabled. Note that the computation time is heavily influenced by the indegree and outdegree of the code areas in the call graph. A higher number of relationships surrounding an application part leads to a higher number of search combinations, which the vulnerability analysis has to try and take into account. For instance, click_count is directly used by only 2 application parts and its analysis takes only 1.4 seconds, while lmem_flip_card() is related to 16 application parts and its analysis takes 322.4 seconds.

The framework found 110 attacks on the assets, which reduces to only 53 unique attacks if we discard the attack step order (see Section 2). For the risk analysis we opted to use an 'amateur' expertise level due to the type of the example application. The risks columns in the table respectively list the risk of the most dangerous attack than can be mounted against an asset and the mitigated risk by using the strongest protection technique supported by our approach (also shown in the table).

Most of the attacks have a high risk to be performed even by an amateur attacker, but using the techniques suggested by our framework all of them can be nearly avoided reducing their risks to low. For instance, the attack path ( statLoc(c2), statCh(c2), ch(c2), br(exCor, c2) ) (Fig. 6) against the execution correctness of lmem_from_Little_One() has a high risk to be executed. However, our implementation has detected that using the code guards technique will lower the risk to low since the attack step statCh(c2) will be severely hindered.

Related Works

The vulnerability assessment is a common issue for different and interdisciplinary fields of research. In the same way, knowledge base decision support systems are employed in several fields that need to take a decision based on a large amount of pre-collected information. For this reason, several projects have been proposed in literature. However, to our knowledge there are no works that completely matches what we have discussed so far. In this section we present some of the works that are relevant to our discussion. Works can be categorized as ontologybased, Petri net and graph based, and web-based systems.

Ontology-based Systems

Applied to risk management, Ekelhart et al. presented a ontology-based system that aims at acting as a decision support system [START_REF] Ekelhart | Ontology-based decision support for information security risk management[END_REF]. The work proposed by the authors relies on a methodology, called AURUM (AUtomated Risk and Utility Management), which is used to perform risk estimation, risk reduction and defense cost estimation. The expert system proposed by the authors is able to support decisions in risk analysis, mitigation and safeguard evaluation.

Fenz et al. have proposed an expert system aiming at semi-automatically inferring the needed controls to protect a system using an ontology. The expert system, named FORISK [START_REF] Fenz | Forisk: Formalizing information security risk and compliance management[END_REF], is the result of an extension of two their previous works [START_REF] Ekelhart | Formalizing information security knowledge[END_REF], [START_REF] Fenz | Information security risk management: In which security solutions is it worth investing[END_REF]. It is a formal representation of information security standards, risk determination and automated identification of countermeasures.

Petri Nets

Dalton et al. have shown that it is possible to model and probabilistically analyse attack trees by using Petri nets [START_REF] Dalton | Analyzing attack trees using generalized stochastic petri nets[END_REF]. This method aims at automatically simulate the system behavior and, alongside the attack tree methodology, identify the proper countermeasures.

Dahl et al. introduced an interval timed coloured Petri net based mechanism that is able to analyse multi-agent and multi-stage attacks [START_REF] Dahl | Modeling and execution of complex attack scenarios using interval timed colored petri nets[END_REF]. The proposed method automatically identifies vulnerabilities in network-based systems.

Coloured Petri nets have been also used by Wu et al. to model hierarchical attacks. Attacks are subdivided into high level and low level attacks. The former ones represent all the paths and the system vulnerabilities exploited to perform the attack. Based on this modelling it is possible to deduce attack cost estimation and risk measurements. The latter ones use separated coloured Petri nets to describe the details of the attack transitions. This level enhance the attack understanding and the effective countermeasure identification.

Yao et al. have recently proposed a Petri net based mechanism to analyse SDN threats [START_REF] Yao | Network security analyzing and modeling based on petri net and attack tree for sdn[END_REF]. In the proposed mechanism they use Petri nets to model the SDN structure and data flow. Then, they employs attack trees to model the attacks. Anyway, they only proposed a method for modelling attacks without delivering any mechanism to deduce countermeasures or cost evaluations.

Web-based and Bayesian Network

Xie et al. based their network security analysis under uncertainty on Bayesian networks [START_REF] Xie | Using bayesian networks for cyber security analysis[END_REF]. This approach aims at improving the enterprise security analysis. They built the Bayesian network on the security graph model. They tested and validated the approach using attack semantics and experimental studies. They also demonstrated that the system does not suffer parameter perturbation.

A Bayesian network based risk management framework have been proposed by Poolsappasit et al. [START_REF] Poolsappasit | Dynamic security risk management using bayesian attack graphs. Dependable and Secure Computing[END_REF]. The framework allows system administrators to evaluate the chance of network compromises, foreseeing how to mitigate and managing them. The system relies on a genetic algorithm that can perform single and multiple objective optimization of security administrator objectives.

A comparison of common methods for security information sharing has been performed by Steffan et al. [START_REF] Steffan | Collaborative attack modeling[END_REF]. They evaluated the capabilities of the systems in supporting avoidance and discovering of vulnerabilities. Finally, they suggested a method based on collaborative attack modelling. The proposed methodology combines graph-based attack modelling with a collaborative web-based tool.

Basset et al. developed a method to analyse network security based on probabilistic graphs [START_REF] Bassett | System and method for cyber security analysis and human behavior prediction[END_REF] modeling actors, events and attributes of a network as nodes. Then, an estimate is associate to each node; it represents the ease of realizing the event, condition or attribute of the node. Attacks are modelled as paths in the graph that reach compromising conditions. They finally associate a probability to each edge in the attack paths thus allowing the final attack chance.

Conclusions and Future Work

In this paper we have extended the work initially proposed in [START_REF] Basile | Automatic discovery of software attacks via backward reasoning[END_REF]. Our approach semi-automatically constructs a representation of an application source code, searches the attacks against software assets and identifies the protections that can mitigate them, performing a risk analysis and protection evaluation cycle.

We have shown that our implementation is able to infer a great number of attacks that could be probably be identified by manual inspection of the code in a very long time. Based on this information, it assesses the risks against the application assets. Furthermore, our inference engine suggests if a protection can mitigate an attack, hence it is able to propose how to protect an application in an automatic way and estimates the residue risk, with minimal user intervention.

For the future, we aim to boost the performance of our approach and support more complex inference rules. We are planning to add the support to suggest an optimal sequence of protections that can be applied to an application, taking into account their synergies (protections that are known to work well when applied on the same assets) and their suggested order of application of the protections.

Fig. 1 .

 1 Fig. 1. General work-flow of our approach.

Fig. 2 .

 2 Fig. 2. Diagram showing the application parts relationships.

Fig. 3 Fig. 3 .

 33 Fig. 3. UML class diagram of the application meta-model.

  Application ::= ApplicationPart * ; ApplicationPart ::= Datum | CodeArea; Datum ::= DatumType ID("{"

Fig. 4 .

 4 Fig. 4. Grammar of the Application Description Language (ADL).

Fig. 5 .

 5 Fig. 5. Assets description in ADL.

Fig. 6 .

 6 Fig. 6. Diagram showing the attack paths breaching the execution correcteness of the lmem_from_Little_One function.

Table 1 .

 1 Table 1 summarizes our results on the application where C W stands for weak confidentiality, I for integrity and E for execution correctness. Memory game attack statistics.

	assets part	attacks property total uniques initial mitigated risks	chosen protection
	click_count	I	2	2 medium	low	anti-debugging
	lmem_from_Little_One() E	12	6	high	low	code guards
	lmem_flip_card()	E	37	16	high	low remote attestation
	lmem_level	I	3	3 medium	low	code mobility
	lmem_state	C W	20	8	high	low	code guards
	lmem_state	I	4	4	high	low	anti-debugging
	lmem_Newgame()	E	32	14	high	low remote attestation
	total		110	53	-	-

See the example in[START_REF] Basile | Automatic discovery of software attacks via backward reasoning[END_REF] for more details on the OTP generator application.

We have disinguished compromission from tampering as their purpose is different. When tampering with an application the attacker modifies the application code to achieve a goal or remove a protection on his own copy, compromission includes

The π(AP i , ǫ) in Eq. 1 is the probability that an attacker with expertise ǫ is able to successfully complete of the attack path. Note that, in estimating the probability to successfully mount an attack path, we consider the probabilities that an attacker with expertise ǫ is able to successfully execute all the attack steps needed to complete it, that is, π(AP i , ǫ) = f (π(AS i,j , ǫ)). The idea behind this formula is that an attacker, to successfully complete an attack path, must correctly undertake all the steps constituting it. We have tested our approach with f = min (the one that gave us best results), with an unrealistic but very conservative f = max, and with f = •.

In practice, we assume that the whole asset weight assigned by the user is gained by the attacker when all the security properties are compromised.

Acknowledgements. The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement number 609734.