A Library Modeling Language for the Static Analysis of C Programs

Abstract

We present a specification language aiming at soundly modeling unavailable functions in a static analyzer for C by abstract interpretation. It takes inspiration from Behavioral Interface Specification Languages popular in deductive verification, notably Frama-C’s ACSL, as we annotate function prototypes with pre and post-conditions expressed concisely in a first-order logic, but with key differences. Firstly, the specification aims at replacing a function implementation in a safety analysis, not verifying its functional correctness. Secondly, we do not rely on theorem provers; instead, specifications are interpreted at function calls by our abstract interpreter.

We implemented the language into Mopsa, a static analyzer designed to easily reuse abstract domains across widely different languages (such as C and Python). We show how its design helped us support a logic-based language with minimal effort. Notably, it was sufficient to add only a handful transfer functions (including very selective support for quantifiers) to achieve a sound and precise analysis. We modeled a large part of the GNU C library and C execution environment in our language, including the manipulation of unbounded strings, file descriptors, and programs with an unbounded number of symbolic command-line parameters, which allows verifying programs in a realistic setting. We report on the analysis of C programs from the Juliet benchmarks and Coreutils.

This work is partially supported by the European Research Council under Consolidator Grant Agreement 681393 — MOPSA.

1 Introduction

Sound static analysis of real-world C programs is hampered by several difficult challenges. In this work, we address the key problem of analyzing calls to external library functions, when analyzing library code is not an option (e.g., it is unavailable, has unsupported features such as system calls or assembly). More specifically, we target the GNU implementation of the C library [13], a library used in a large number of applications and featuring thousands of functions covering various aspects, such as file management, socket communication, string processing, etc. Several approaches have been proposed to analyze programs that depend on such complex libraries:

Fig. 1.

Examples of stubs in different analyzers.

Stubs as C Code. A common solution is to provide alternative C implementations of the library functions, called stubs. In order to remain sound and be effectively analyzed, stubs are generally simpler and contain calls to special builtins of the analyzer that provide more abstract information than the classic constructs of the language. This approach is adopted by many static analyzers, such as Astrée [4] and Infer [6]. For example, Fig. 1a shows the stub of in Infer: it uses builtin functions to check that the argument points to a valid block before returning its allocation size. The approach makes it difficult for the stub programmer to express complex specifications with higher levels of abstractions, as key parts of the semantics are hidden within the builtin implementation. Moreover, writing stubs as C code and hard-coding builtins is acceptable when targeting embedded code [4], that does not rely much on libraries, but is not scalable to programs with more dependencies.

Stubs as Logic Formulas. More adapted specification languages have been proposed to overcome these drawbacks, principally based on formulas written in first-order logic. Some of them exploit the flexibility of the host language in order to define an embedded domain specific language, such as CodeContracts checker [11] that can express specifications of C# functions in C# itself. Other solutions propose a dedicated language and specifications are written as comments annotating the function. The most notable examples are JML for Java [18] and ACSL for C [3]. They have been widely used in deductive verification, employing theorem provers that naturally handle logic-based languages, but less in value static analysis by abstract interpretation. We show in Fig. 1b the specification of in ACSL, as defined by Frama-C’s value analyzer [9]. The syntax is less verbose than the C counterpart. Yet, essential parts of the stub are still computed through builtins. It is worth noting that Frama-C features another, more natural, specification of , exploiting the expressiveness of the logic to avoid builtins. But this specification is large (64 lines) and employs quantified formulas that are too complex for the value analysis engine: it is used only by the deductive verification engine.

Abstract Interpretation of Logic Formulas. In this paper, we propose a novel approach based on abstract interpretation [7] that can interpret specifications written in a logic-based language of library functions when they are called. Similarly to CodeContracts checker [11], we do not rely on theorem provers to interpret formulas; instead, specifications are interpreted by abstract domains tailored to this task. The key novelty of our solution is that we consider the logic language as a separate language with its own concrete and abstract semantics, while contracts in cccheck are embedded within the host language as function calls. We believe that this decoupling makes the design more generic and the language is not limited by the semantic nor the syntax of the host language.

We implemented the proposed approach into Mopsa [16], a static analyzer that features a modular architecture that helps reusing abstract domains across different languages. We leverage this modularity and we illustrate how we can improve the analysis by extending C abstract domains to add transfer functions that exploit the expressiveness of formulas and infer better invariants. For example, the stub of as defined in Mopsa is shown Fig. 1c. It relies essentially on constraints expressed as formulas instead of specific analyzer builtins. These formulas can be handled by Mopsa, and string lengths can be computed precisely even in the case of dynamically allocated arrays. For instance, at the end of the program shown in Fig. 1d, Mopsa can infer that .

Contributions. In summary, we propose the following contributions:

• We present in Sect. 2 a new specification language for C functions and we formalize it with an operational concrete semantic. In addition to standard constructs found in existing languages, it features a resource management system that is general enough to model various objects, such as blocks allocated by or file descriptors returned by . Illustrative examples can be found in Appendix A.

• We present in Sect. 3 a generic abstract domain for interpreting the specification language, that is agnostic of the underlying abstraction of C.

• In Sect. 4, we illustrate how a string abstraction can benefit from the expressiveness of the specification language in order to provide better invariants.

• We implemented the analysis in Mopsa and we modeled over 1000 library functions. In Sect. 5, we report on the results of analyzing some Juliet benchmarks and Coreutils programs. More particularly, we show how our analysis combines several symbolic domains in order to analyze C programs with an unbounded number of command-line arguments with arbitrary lengths. To our knowledge, Mopsa is the first static analyzer to perform such an analysis.

Limitations. The following features are not supported by our analysis: recursive functions, longjumps, bitfields, inline assembly, concurrency and multi-dimensional variable length arrays.

2 Syntax and Concrete Semantics

We define the syntax and operational concrete semantics of the modeling language. The syntax is inspired from existing specification languages, such as ACSL [3] and JML [18], with the addition of resource management. The semantics expresses a relation between program states before the function call and after.

Fig. 2.

Syntax of the modeling language.

2.1 Syntax

The syntax is presented in Fig. 2. It features two kinds of statements:

• Side-effect statements specify the part of the input state which is modified by the function: specifies that a variable (or an array slice) is modified by the function; creates a fresh resource instance of a specified class ($ident$) and assigns its address to a local variable; conversely, destroys a previously allocated resource. Any memory portion that is not explicitly mentioned by these statements is implicitly assumed to be unchanged. Resources model dynamic objects, such as memory blocks managed by and , or file descriptors managed by and . The models of these functions can be found in Appendix A. Assigning a class to resources allows supporting different attributes (e.g., read-only memory blocks) and allocation semantics (e.g., returning the lowest available integer when allocating a descriptor, which is needed to model faithfully the function).

• Condition statements express pre and post-conditions: defines mandatory conditions on the input environment for the function to behave correctly; defines assumptions, and is used for case analysis; expresses conditions on the output environment (the return value, the value of modified variables, and the size and initial state of allocated resources).

Cases. We support a disjunctive construct (akin to Frama-C’s behaviors) to describe functions with several possible behaviors. Each case is independently analyzed, after which they are all joined. Statements placed outside cases are common to all cases, which is useful to factor specification. For the sake of clarity, we will focus on the formalization of stubs without cases.

Formulas and Expressions. Formulas are classic first-order, with conjunctions, disjunctions, negations and quantifiers. The atoms are C expressions (without function call nor side-effect), extended with a few built-in functions and predicates: $e \in set$ restricts the range of a numeric value or the class of a resource; checks whether a resource has not been freed; given a pointer e, returns a pointer to the beginning of the memory block containing e, is the block size, and is the byte-offset of e in the block.

2.2 Environments

Concrete memories are defined classically. The memory is decomposed into blocks: , which can be either variables in $\mathcal {V}$ or heap addresses in $\mathcal {A}$. Each block is decomposed into scalar elements in , where denotes the memory region in block b starting at offset o and having type $\tau$. A scalar element of type $\tau$ can have values in $\mathbb {V}_\tau$, where $\mathbb {V}_\tau$ is $\mathbb {R}$ for numeric types and is a block-offset pair for pointers¹. The set of all scalar values is .

Environments, in , encode the state of the program using: a memory environment in , mapping scalar elements to values, and a resource environment in , which is a partial map mapping allocated resources to their class, size, and liveness status (as a Boolean).

Example 1

Given the declaration: , the environment:

encodes the state where field has value 5 and points to a resource containing two elements with values 3 and $-1$ respectively.

2.3 Evaluation

Fig. 3.

Concrete semantics of expressions.

Fig. 4.

Concrete semantics of formulas.

Expressions. The evaluation of expressions, given as , returns the set of possible values to handle possible non-determinism (such as reading random values). It is defined by induction on the syntax, as depicted in Fig. 3. The stub builtin reduces to the C builtin for variables and returns the size stored in the resource map for dynamically allocated blocks. Calls to and evaluate their pointer argument and extract the first (respectively second) component. To simplify the presentation, we do not give the explicit definition of the C operators, which is complex but standard. Likewise, we omit a precise treatment of invalid and pointers (see [19] for a more complete definition). Finally, we omit here reporting of C run-time errors.

Formulas.

The semantics of formulas , shown in Fig. 4, returns the set of environments that satisfy it. It is standard, except for built-in predicates: to verify the predicate $e \in R$ (resp. ), we resolve the instance pointed by e and look up the resource map to check that its class equals R (resp. its liveness flag is $true$).

2.4 Relational Semantics

Statements express some information on pre and post-conditions, that is, on the relation between input and output environments.

Expressions and Formulas. To allow expressions to mention both the input and output state, we use the classic prime notation: $e'$ denotes the value of expression e in the post-state. Denoting $\tilde{expr}$ the set of expressions with primes, their semantic on an input-output environment pair is given by . Figure 5 presents the most interesting cases: evaluating a primed dereference reduces to the non-relational evaluation on , while a non-primed dereference reduces to on . The case of and is similar. Other cases are analog to non-relational evaluation.

Fig. 5.

Concrete semantics of relational expressions.

We denote by $\tilde{ form }$ formulas with primes, and define their evaluation function as returning a relation. As shown in Fig. 6, to evaluate predicates $e \in R$ and , only input environments are inspected, as the resource class is an immutable property and the liveness flag can be changed only by statements in previous calls. The remaining definitions are similar to the non-relational case.

Fig. 6.

Concrete semantics of relational formulas.

Example 2

Consider again variable v̧ shown in Example 1 and the following relational formula: . When applied on the previous environment we obtain the relation:

Side-effect Statements. We model side-effect statements as relation transformers, shown in Fig. 7. Given an input-output relation as argument, it returns a new relation where the output part is updated to take into account the effect of the statement. Thus, starting from the identity relation, by composing these statements, we can construct a relation mapping each input environment to a corresponding environment with resources allocated or freed, and variables modified. The statement allocates a new instance of resource class R and assigns its address to variable v. The function returns the set of scalar types and their offsets within a given type. We have no information on the block size (except that it is a non-null multiple of the size of $\tau$) nor the block contents; both information can be provided later using an statement. The statement modifies the memory block pointed by e and fills the elements located between indices a and b with unspecified values. Finally, frees the resource pointed by e by updating its liveness flag. These statements only use non-primed variables, hence, all expressions are evaluated in the input part of the relation, which is left intact by these transformers.

Condition Statements. A condition statement adds a constraint to the initial input-output relation built by the side-effect statements. We define their semantics as a function . Another role of these statements is to detect specification violation (unsatisfied ). Thus, we enrich the set of output environments with an error state $\varOmega$, so that denotes an input environment that does not satisfy a pre-condition. The semantics is given in Fig. 7. Both and statements use the simple filter as they operate on input environments. In contrast, statements express relations between the input and the output and use therefore the relational filter . Combining two conditions is a little more subtle than intersecting their relations, due to the error state. We define a combination operator that preserves errors detected by conditions. Due to errors, conditions are not commutative. Indeed is not equivalent to , as the later will report errors when $x\ne 0$.

Fig. 7.

Concrete semantics of statements.

Fig. 8.

Concrete semantics of the stub.

Iterator. Figure 8 shows the semantic function of a complete stub. It first executes its side-effect statements only , then condition statements , and finally applies the resulting relation $R_2$ to the initial states at function entry I. It returns two sets of environments: the environments O at function exit when pre-conditions are met, and the environments X at function entry that result in a violation of a pre-condition.

3 Generic Abstract Semantics

We show how an existing abstract domain for C can be extended to abstract the concrete semantics of our stubs in a generic way. The next section will focus on specific abstractions exploiting more finely the structure of stub statements.

3.1 Abstract Domain

C Domain. We assume we are given an abstract domain of memories with the standard operators: least element , join , and widening , as well as a sound abstraction for classic memory statement , including: $x\leftarrow y$, to model assignments of C expressions; $forget (b,x,y)$, to assign random values to a byte slice [x, y] of a memory block b; $add (b)$, to add a memory block with random values; $remove (b)$ to remove a memory block; and the array sumarization operators $expand (b_1,b_2)$ and $fold (b_1,b_2)$ from [14]. $expand (b_1,b_2)$ creates a weak copy $b_2$ of block $b_1$, i.e. both $b_1$ and $b_2$ have the same constraints without being equal. For example, executing $expand (x,z)$ when $x \ge y \wedge x \in [1,10]$ yields $x \ge y \wedge x \in [1,10] \wedge z \ge y \wedge z \in [1,10]$. The converse operation, $fold (b_1,b_2)$, creates a summary in $b_1$ by keeping only the constraints also implied by $b_2$, and then removes $b_2$. We exploit them to abstract unbounded memory allocation and perform weak updates.

Heap Abstraction. We also assume that we are given an abstraction of heap addresses $\mathcal {P}(\mathcal {A})$ into a finite set of abstract addresses, with least element and join . Classic examples include call-site abstraction, and the recency abstraction [2] we use in our implementation. An abstract address may represent a single concrete address or a (possibly unbounded) collection of addresses, which is indicated by a cardinality operator . Finally, we assume the domain provides an allocation function . As an abstract allocation may cause memory blocks to be expanded or folded, and the pointers to point to different abstract addresses, the function also returns an updated memory environment.

Environments. For each abstract block in , we maintain its byte size in a numeric variable in the memory environment, and track its possible resource classes in $\mathcal {P}(\mathcal {C})$, and possible liveness status in the boolean lattice $\mathcal {P}(\{ true , false \})$. The abstraction of environment sets is thus:

(1)

The , , and operators are derived naturally from those in and , and we lift C statements to .

3.2 Evaluations

Our abstraction leverages the modular architecture and the communication mechanisms introduced in the Mopsa framework [16]. We will employ notably symbolic and disjunctive evaluations, which we recall briefly.

Expressions. In the concrete semantics, expressions are evaluated into values. Abstracting expression evaluation as functions returning abstract values, such as intervals, would limit the analysis to non-relational properties. Instead, domains in Mopsa can evaluate expressions into other expressions: based on the current abstract state, expression parts are simplified into more abstract ones that other domains can process. A common example is relying on abstract variables. For instance, the memory domain will replace a expression into the variable after determining that e points to block b, producing a purely numeric expression. Communicating expressions ensures a low coupling between domains, while preserving relational information (e.g., reduces to comparing two numeric variables, and i). A domain can also perform a case analysis and transform one expression into a disjunction of several expressions, associated to a partition of the abstract state (e.g., if e can point to several blocks). Formally, a domain implements expression evaluation as a function: . To express concisely that the rest of the abstract computation should be performed in parallel on each expression and then joined, we define here (and use in our implementation) a monadic bind operator:

(2)

We illustrate formally abstract expression evaluation on the expression. First, the pointer domain handles the pointer expression e: returns a set of triples $(b,o,\varepsilon ')$ where b is an abstract block, o a numeric offset expression, and $\varepsilon '$ the part of $\varepsilon$ where e points into block b. Thanks to this disjunction, the abstract semantics of follows closely the concrete one:

(3)

Formulas. Evaluation of formulas is defined by the function , shown in Fig. 9. We focus on the most interesting cases which are the quantified formulas. Existential quantification reduces to assigning to v the interval [a, b] and keeping only environments that satisfy f. Universal quantification are handled very similarly to a loop . We perform an iteration with widening for v from a to b and we over-approximate the sequence of states statisfying f. The overall formula is satisfied for states reaching the end of the sequence. These generic transfer functions can be imprecise in practice. We will show later that specific domains can implement natively more precise transfer functions for selected quantified formulas.

Fig. 9.

Abstract semantics of formulas.

Relations. The concrete semantics requires evaluating expressions and formulas not only on states, by also on relations. To represent relations in the abstract, we simply introduce a family of primed variables: returns the primed version of a block (i.e., the block in the post-state). This classic technique allows lifting any state domain to a relation domain. Combined with relational domains, we can express complex relationships between values in the pre- and the post-state, if needed. The relation abstractions and of and can be easily expressed in terms of the state abstractions and we already defined. As an example, the evaluation of a primed dereference simply evaluates e into a set of memory blocks b and offset expressions o, and outputs a dereference of the primed block at the (non-primed) offset expression o, which can be handled by the (relation-unaware) memory domain:

(4)

3.3 Transfer Functions

Fig. 10.

Abstract semantics of statements.

Side-effect Statements. The effect of a statement is approximated by defined in Fig. 10. Resource allocation first asks the underlying heap abstraction for a new abstract address with , which is bound to a new variable v; a new size variable is created and the resource map is updated with the class and liveness information. The block is also initialized with random values using $forget$. Assignments reduces to $forget$ on the primed version of the block b e points to (recall that the output value is specified by a later ). Finally, resets the liveness flag of the primed block.

Condition Statements. The abstract semantics of condition statements is given by , defined in Fig. 10. The function returns a pair of abstract environments: the first one over-approximates the output environments satisfying the condition, while the second one over-approximates the input environments violating mandatory conditions specified with statements.

Fig. 11.

Abstract semantics of the stub.

Iterator. The abstract semantic of a whole stub is defined in Fig. 11. First, the $expand$ function is used to construct an identity relation over the input abstract state $\varepsilon ^\sharp _0$. To improve efficiency, this is limited to the blocks that are effectively modified by the stub; this set is over-approximated using the function, which resolves the pointer expressions occurring in statement. Then, side-effect statements are evaluated. Note that, for an statement, while whole blocks pointed by a are duplicated in the output state, only the parts in the [x, y] range are assigned random values. Condition statements are then executed, collecting contract violation and refining the output state. Finally, we remove the unprimed version of primed (i.e., modified) blocks and the primed block into its unprimed version, thus reverting to a state abstraction that models the output state. In case of a primed block b modeling several concrete blocks (i.e., ), the primed block is folded into the unprimed version, so as to preserve the values before the call, resulting in a weak update.

4 Specific Abstract Semantics: The Case of C Strings

We now show how we can design a formula-aware abstract domain, with an application to C string analysis. The domain handles precisely selective quantified formula, while reverting in the other cases (as all other domains) to the generic operators.

String Length Domain. Strings in C are arrays of elements containing a delimiting null byte indicating the end of the string. Many functions in the standard C library take strings as arguments and assume they contain a null byte delimiter. We want to express and check this assumption in the function stubs. We exploit a classic abstraction already present in Mopsa: the StringLength domain [17] that maintains a numeric abstract variable for arrays to store the offset of the first null byte. It thus infers, for each array a, an invariant of the form:

(5)

Example 3

Consider the following example, where n ranges in [0, 99]:

An analysis with the Intervals domain will infer that . Adding the Polyhedra domain, we will moreover infer that .

Stub Transfer Functions. Within a stub, a pre-condition stating the validity of a string pointed to by an argument named s is naturally expressed as:

(6)

Proving this requirement requires checking the emptiness of its negation, which involves a universal quantifier. Using the generic abstraction from last section, it is equivalent to proving emptiness after the loop . This, in turn, requires an iteration with widening and, unless s has constant length, a relational domain with sufficient precision, which is costly.

Table 1. Transfer functions of formulas in the string length domain.

To solve these problems, we propose a direct interpretation of both formulas in the string domain, i.e., we add transfer functions for and ,² as shown in Table. 1. They perform a case analysis: the abstract state ${\epsilon }^\sharp$ is split into two cases according to a condition, and we keep all environments in one case ( ) and none in the other ( ). For instance, assuming that (5) holds, then Case #1 of states that the quantification range [lo, hi] covers only elements before the null byte, so that the formula does not hold. Case #2 states that there is a value in [lo, hi] greater than or equal to the string length, in which case s[i] may be null and the formula may be valid. Similarly, Case #1 of arises when the null byte is outside the quantification range, so that the formula may be valid. In Case #2, the null byte is in the range, and the formula is definitely invalid. We stress on the fact that all the conditions are interpreted symbolically in the numeric domain; hence, lo and hi are not limited to constants, but can be arbitrary expressions.

Example 4

Let us illustrate how the predicate (6) can be verified on the following abstract environment:

(7)

which represents the case of a variable s pointing to a resource instance @ allocated by with at least one byte. The string domain indicates that the position of the null byte is between 0 and . When checking the formula , the condition for Case #1 never holds since:

When checking its negation, , Case #1 is also unsatisfiable, for the same reason. As the transformer for Case #2 returns $\bot$, the overall result is $\bot$, proving that Requirement (6) holds: the stub does not raise any alarm.

Genericity of Formulas. An important motivation for using a logic language is to exploit its expressiveness within abstract domains to analyze several stubs with the same transfer functions. We show that this is indeed the case: the transfer function that was used to validate strings in the previous section can be used, without modification, to compute string lengths.

Example 5

Let us go back to the example of the function defined as:

and consider again the environment (7). As shown before, the statements at line 3 validating the string do not raise any alarm. At line 5, the classic transfer functions of the StringLength domain [17] infer that:

since and is the position of the first null byte. Finally, at line 6, both cases of the second transfer function in Table 1 are valid. Since we keep a non-$\bot$ post-state only for Case #1, we obtain:

hence the domain precisely infers that returns the length of string @.

5 Experiments

We implemented our analysis in the Mopsa framework [16]. It consists of 29503 lines of OCaml code (excluding parsers). Among them, 16449 lines (56%) are common with analyses of other languages, such as Python. C domains consist of 11342 lines (38%) and the stub abstraction consists of 1712 lines (6%).

We wrote 14191 lines of stub, modeling 1108 functions from 50 headers from the Glibc implementation of the standard C library, version 8.28 [13]. All stubs thoroughly check their arguments (pointers, strings, integers, floats), soundly model their side effects, dynamic memory allocation, open files and descriptors. We refrained form implicit assumptions, such as non-aliasing arguments. At an average of 8 meaningful lines per stub, the language proved to be concise enough. Some examples can be found in Appendix A.

To assess the efficiency and the precision of our implementation, we target two families of programs. We run our analysis on part of NIST Juliet Tests Suite [5], a large collection of small programs with artificially injected errors. These tests are precious to reveal soundness bugs in analyzers, but do not reflect real-world code bases. Hence, we also target more realistic programs from the Coreutils package [12], which are widely used command-line utilities. These programs, while not very large, depend heavily on the C standard library. We run all our tests on an Intel Xeon 3.40 GHz processor running Linux.

5.1 Juliet

Table 2. Analysis results on Juliet. : precise analysis, : analysis with false alarms.

The Juliet Tests Suite [5] is organized using the Common Weakness Enumeration taxonomy [1]. It consists of a large number of tests for each CWE. Each test contains bad and good functions. Bad functions contain one instance of the CWE, while good functions are safe.

We selected 12 categories from NIST Juliet 1.3 matching the safety violations detected by Mopsa. For each test, we have analyzed the good and the bad functions and measured the analysis time and the number of reported alarms. Three outcomes are possible. The analysis is precise if it reports (i) exactly one alarm in the bad function that corresponds to the tested CWE, and (ii) no alarm in the good function. The analysis is unsound if no alarm is reported in the bad function. Otherwise, the analysis is imprecise.

The obtained results are summarized in Table 2. From each category, we have excluded tests that contain unsupported features or that do not correspond to runtime errors. As expected, all analyses are sound: Mopsa detects the target CWE in every bad test. However, half of the tests were imprecise. Much of this imprecision comes from the gap between Mopsa’s error reporting and the CWE taxonomy. For instance, an invalid string passed to a library function may be reported as a stub violation while Juliet expects a buffer overflow. By considering precise an analysis reporting no alarm in the good function and exactly one alarm in the bad function (without considering its nature), the overall precision increases to 71% (e.g. 89% of CWE121 tests become precise). Other factors also contribute to the imprecisions, such as the lack of disjunctive domains. Finally, many tests use the socket API to introduce non-determinism, and the current file management abstraction was not precise enough to prove the validity of some file descriptors.

5.2 Coreutils

Our second benchmark includes 19 out of 106 programs from Coreutils version 8.30 [12]. Each program consists in a principal C file containing the function, and library functions that are shared among all Coreutils programs. Due to these complex dependencies, it was difficult to extract the number of lines corresponding to individual programs. Instead, we computed the number of atomic statements, consisting of assignments and tests (e.g. in and statements), in the functions reached by the analysis. This gives an indication of the size of the program, but the scale is not comparable with line count metrics.

Fig. 12.

Analysis results on Coreutils programs.

Scenarios. Three scenarios were considered. The first one consists in analyzing the function without any argument. In the second scenario, we call with one symbolic argument with arbitrary size. The last scenario is the most general: is called with a symbolic number of symbolic arguments.

Abstractions. For each scenario, four abstractions were compared. In the first abstraction $A_1$, we employed the Cells memory domain [19] over the Intervals domain. The second abstraction $A_2$ enriches $A_1$ with the StringLength domain [17] improved as discussed in Sect. 4. The third abstraction $A_3$ enriches $A_2$ with the Polyhedra domain [8, 15] with a static packing strategy [4]. Finally, $A_4$ enriches $A_3$ with a PointerSentinel domain that tracks the position of the first pointer in an array of pointers; it is similar to the string length domain and useful to represent a symbolic and handle functions such as (see Appendix A.4).

Limitations. The analysis of recursive calls is not yet implemented in Mopsa. We have found only one recursive function in the analyzed programs, which we replaced with a stub model. The second limitation concerns the family of functions. We have not considered the case where these functions modify the array by rearranging its elements in some specific order, since such modifications make the analysis too imprecise. However, we believe that this kind of operation can be handled by an enhanced PointerSentinel domain. This is left as future work.

Precision. Figure 12a shows the number of alarms for every analysis. The most advanced abstraction $A_4$ reduces significantly the number of alarms, specially for the fully symbolic scenario. This gain is not due to one specific abstraction, but it comes from the cooperation of several domains, most notably between Polyhedra and StringLength. This also emphasizes the effectiveness of domain communication mechanisms within Mopsa [16], notably symbolic expression evaluation.

Efficiency. As shown in Fig. 12b, the gain in precision comes at the cost of degraded performances. The most significant decrease corresponds to the introduction of the $\textsc {Polyhedra}$ domain. Note that our current packing strategy is naive (assigning for each function one pack holding all its local variables); a more advanced strategy could improve scalability.

Coverage. We have also measured the ratio of statements reached by the analysis in the three scenarios. While not a formal guarantee of correctness, a high level of coverage provides some reassurance that large parts of the programs are not ignored due to soundness errors in our implementation or our stubs. We discuss only the case of abstraction $A_4$, as other cases provide similar results. Figure 12c presents the results. In most cases, using one symbolic argument helps covering a significantly larger part of the program compared to analyzing main without any argument. Coverage with one or several symbolic arguments is roughly the same, possibly due to the control flow over-approximations caused by even a single symbolic argument. Nevertheless, only the last scenario, covering an unbounded number of arguments, provides a soundness guarantee that all the executions of the program are covered. As far as we know, this is not supported in the static value analyses by Frama-C [10] nor Astrée [4].

6 Conclusion

We presented a static analysis by abstract interpretation of C library functions modeled with a specification language. We defined an operational concrete semantics of the language and proposed a generic abstraction that can be supported by any abstract domain. We also showed how a C string domain could be enriched with specialized transfer functions for specific formulas appearing in stubs, greatly improving the analysis precision. We integrated the proposed solution into the Mopsa static analyzer and experimented it on Juliet benchmarks and Coreutils programs. In the future, we plan to extend our coverage of the standard C library, provide models for other well-known libraries, such as OpenSSL, and experiment on larger program analyses. In addition, we envisage to upgrade our specification language to support more expressive logic. Finally, we want to improve the quality of our results by adding more precise abstractions, such as trace partitioning, or more efficient modular iterators.

A Stub Examples

This appendix presents additional representative examples of the stubs we developed for the GNU C library.

1.1 A.1 Predicates

To simplify stub coding, following other logic-base specification languages, Mopsa allows defining logic predicates, that can be then used in stubs. For instance, we define the following useful predicates on C strings: valid_string(s) states that s is zero-terminated, and is useful as argument precondition; in_string(x,s) states that x points within string s before its null character, which is useful to state post-conditions.

1.2 A.2 Memory Management

Memory allocation functions show examples of resource allocation, and the use of cases to simplify the specification of functions with several behaviors.

1.3 A.3 File Descriptors

File descriptors are another example of resource allocation, but use a specific class that the analyzer can track to allocate integer file descriptors according to the C library policy: the least unused integer is picked. This allows modeling precisely patterns such as close(0); int f = open("...");. read reads non-deterministic values, after checking that the file has been opened and not closed.

1.4 A.4 Command-Line Arguments

We provide the simplified model of the getopt function we used in Coreutil analyses.