Abstract
In 
Introduction
The C programming language is considered as the de facto standard for system programming. The main reasons of its success are its performance, flexibility, strong support, and portability. However, security features are either absent or badly supported in C programming. Memory management left to the programmer's discretion are the source of many critical security vulnerabilities. As the number of lines of code grows, manual checking of security violations becomes cumbersome and error-prone for programmers. Therefore, automated tools for vulnerability detection are very helpful in detecting and fixing errors in source code.
There are a range of static analysis techniques [1, 3, 4] used to detect vulnerabilities at early stages of software development. These techniques have not the ability to cover all memory errors since they operate on a conservative approximation of the program. They offer different tradeoffs between the precision and the complexity of the analysis. Our study of static analysis techniques indicates that flow-sensitive analysis and alias analysis are two key factors to precisely detect memory errors. Nevertheless, these factors may increase the complexity of the analysis. The current situation gives us enough room to define a new static analysis approach that offers a good complexity-vsprecision trade-off for detecting memory errors.
In this paper, we describe our automated approach based on flow-sensitive type and alias analysis for detecting temporal memory errors in C programming. More precisely, we target the following programming errors: double freeing a pointer, using a freed pointer, freeing a pointer that has never been allocated, dereferencing NULL/unallocated pointers, assigning uninitialized values. The core idea is to instrument the C standard type system with effect, region, and host annotations in order to collect valuable security information on the analyzed program. The host annotation indicates the state and reveals the actual type of a memory location. The flow-sensitive nature of our approach allows type annotations to change from one program statement to another. Hence, we improve the analysis precision for detecting temporal errors. As in [11] , the flow-sensitivity is restricted to the type annotations in order not to complicate the inference algorithm. Furthermore, we address the pitfalls of indirect assignments by endowing our approach with a flow-sensitive alias analysis [5] . As such, a modification to the annotations of a variable is propagated to all its aliases.
The main contributions of our paper are the following:
• A new type system based on region, effect, and host annotations for detecting memory errors in C source code. We endow our type system with static security checks that use these annotations to verify and ensure the safety of pointers usages.
• A flow-sensitive inference algorithm is defined to automatically infer annotated types to program expressions and statements and to perform the static security checks.
• A prototyped GCC extension that statically typechecks C programs for temporal memory errors.
This paper is organized as follows: Section 2 outlines an informal overview of the different components of our approach. Section 3 presents the effect, region and host annotations for security. In Section 4, we describe the typing rules for expressions, statements, and control flow constructs. Section 5 outlines the static security checks performed during our type analysis. We describe the limitations of our static analysis in Section 6. Section 7 presents our annotations inference algorithm and the proof of the soundness between our inference algorithm and the type system. We illustrate our prototype with a case study in Section 8. We discuss the related work in Section 9. Finally, we draw conclusions in Section 10.
Approach Overview
Our type and effect analysis involves different components that interact in order to detect temporal memory errors as detailed hereafter:
• We extend the standard C type system with annotations in order to collect relevant security information of the analyzed program.
• We define static security checks that use our aforementioned annotations to verify and ensure the safety of pointers usages. Our defined type system is endowed with these security checks to enforce memory safety properties.
• We define flow-sensitive annotated types that are allowed to change from one program statement to another [11] . Notice that a statement that directly changes the annotations of a given location is also indirectly changing the annotations of its aliases. As such, we elaborate a recursive algorithm based on flow-sensitive alias information in order to propagate type annotations updates to all locations directly and indirectly involved in a program statement.
Extending C Type System
This section presents the effect, region, and host annotations that our type system uses to collect valuable security information of the analyzed program.
• The domain of regions is intended to abstract variables' memory locations and dynamic memory locations.
The symbols ρ, ρ represent known values from the regions domain. The symbol stands for currently unknown location. We use the notation {ρ 1 , . . . , ρ n } to represent the set of regions a pointer may refer to.
• The domain of declared types defines a subset of the basic types of the C language.
It includes the empty type void, the integer type, and the pointer type ref (κ).
• The domain of inferred types decorates the declared types with top-level effect, region, and host annotations, i.e, inserted at the outermost constructor.
The pointer type ref ρ (κ) η is annotated with its memory location ρ. The types int η and ref ρ (κ) η have a host annotation η that indicates the content of their related memory location.
• The host annotation indicates the content of a memory location.
The element malloc denotes an allocated pointer. The element free indicates a freed memory location. The value wild denotes unallocated pointer or uninitialized integer. The element &τ stands for a region holding a value of type τ .
• The domain of effects [12] captures the side effect of memory operations.
We use ∅ to denote the absence of effects. The term σ; σ denotes the sequencing of σ and σ . Each effect records the program point of the source code where it is produced. The effect if (σ, σ ) refers to a branching conditions at program point , where the effects σ and σ are produced at the true branch and at the false branch respectively. The effect rec (σ) stands for a recursively defined effect generated in a loop construct at program point . The term alloc(ρ, ) and dealloc(r, ) denotes memory allocation and memory deallocation respectively. The effect arith(r, ) captures arithmetic operations on pointers. The effect read(r, τ, ) describes access to regions in r that holds a value of type τ . The effect assign(r, τ, ) represents the assignment of a value of type τ to regions in r.
The declared types and the inferred types are related through the " " operator: When applied on a declared type κ, it returns an inferred type τ with a host annotation set to [wild] and unknown region location for pointers. On the other hand, the "¯" operator suppresses all the annotations of inferred types. When applied on an if (τ, τ ) type construct, it yields the following: if (τ, τ ) =τ =τ
Syntax
We illustrate our analysis on a core syntax, presented in Figure 1 , that captures the essence of the C language. A program π contains variable declarations, denoted by δ, and program statements, referred to by s. Expressions e comprise lvalues l v and rvalues r v . The rvalues include integer scalar n, dereferencing expression * r v , and arithmetic operation on pointers e op e . The lvalues are access paths 
Typing Rules
In this section, we detail the typing rules of our static semantics. We use in these rules the auxiliary functions: (1) regionof (l v ) that returns the set of regions an lvalue may refer to, (2) hostof (τ ) that returns the host annotation of a type τ . The typing rules for program expressions are presented in Section 4.1, the type judgements for statements are presented in Section 4.2, and Section 4.3 outlines the typing rules for control flow statements. We based our typing rules on the type system for imperative languages in [13] .
Typing Rules for Program and Expressions
The typing rules for expression, defined in Figure 2 , are based on the type annotations and the static security checks defined Section 5. The sequent (δ, s) indicates that the program containing declarations δ and statements s is welltyped. The deduction E δ : E yields a new environment E by adding the declarations δ to environment E. The sequent E , e : τ, σ states that under typing environment E and at program point , the expression e has type τ and the evaluation of e yields the effect σ. Through this paper, we will write E † E to denote the overwriting of E by E , i.e., the domain of E † E is Dom(E) ∪ Dom(E ), and we have
Program and Declarations
, e op e : τ, (σ; σ ; arith(r, ))
Figure 2. Typing rules for program declarations and expressions
The rule (var-decl) maps in E a declared variable of type κ to the annotated typeκ. At variable declarations, region annotations have unknown values and host annotations are set to [wild] . The rule (pointer arith) evaluates pointer arithmetic that is captured by effect arith(r, ), where r is the set of possible regions of the pointer. The rule (pointer deref) dereferences a pointer expression e of type τ , if the check safeRead(_) succeeds. We call the function storedType(τ ) to get the actual type τ from the host annotation of pointer type τ . The dereference operation generates the effect read(r, τ , ).
Typing Rules for Statements
This section presents the typing rules for statements, defined in Figure 3 . We consider memory allocation, memory deallocation and assignment statements. The aforementioned statements modify the type annotations of their related lvalues. To express flow-sensitivity, the statements judgement is of the form E , s, E , σ to express that under typing environment E, the execution of statement s yields a new environment E and produces the effect σ. The recursive algorithm updEnv() used in our typing rules updates the type annotations of an lvalue directly involved in a program statement. It also updates the type annotations of the aliases of that lvalue. For space constraint, we do not illustrate the algorithm of the function updEnv() in this paper. The function updEnv() takes as arguments the current environment E, a statement s, and its program point . Then, it outputs a new environment E' with updated annotations for variables directly and indirectly involved in statement s.
Figure 3. Typing rules for program statements
The rule (free) conservatively deallocates all memory locations in r an lvalue l v may refers to. The deallocation is guarded by the safeFree(_) security check and produces the effect dealloc(r, ). The call to updEnv() yields a new environment E where the host annotation of l v and of all its aliases is set to [free]. The rule (malloc) allocates a fresh memory location ρ for pointer designated by l v and sets its host annotation to [malloc] . We add the effect alloc(ρ, ) for allocating memory region ρ at program point . For the other assignment statements, we invoke the safeWrite(_) check, detailed in Section 5, that verifies that a value of type τ can be assigned to a variable of type τ . If the check succeeds, the function updEnv() propagates the annotations from the rhs operator to the lhs operator. Then, it updates all type annotations of the lhs operator's aliases accordingly. The effect generated for assigning a value of type τ is assign(r, τ, ), where r is the possible set of regions pointed to by l v .
Typing Rules for Control Flow Statements
The rules for control flow statements, defined in Figure  4 , endows our analysis with more precision to detect vulnerabilities.
Control Flow Statements
(seq) E , s1, E , σ1 E , s2, E , σ2 E , s1; s2, E , (σ1; σ2) (cond) E , b : bool, ∅ E , s1, E , σ1 E , s2, E , σ2 E , if b then s1 else s2, E E , if (σ1, σ2) (loop) E , b : bool, ∅ E , s, E , σ E = E † rec (updEnv(E, s, )) E , while b do s, E E , rec (σ)
Figure 4. Typing rules for control flow constructs
The rule (seq) defines the sequencing of statements where the generated effect is the sequencing effect of s 1 and s 2 . For the rule (cond), we introduce the merge operator defined hereafter:
The if (E(x), E (x)) type construct is assigned to variable x at the merge point of the branch condition at program point . It says that variable x is of type E(x) (if the true branch is followed) or of type E (x) (if the false branch is followed). The rule (loop) captures the recursive execution of statements inside a loop construct. The recursive call rec(updEnv(E, s, )) denotes 0 to infinite number of iterations of the loop, where each iteration yields a new environment as defined hereafter:
The effect rec (σ) denotes a recursively (infinite) effect generated by a loop at program point . The environment derived from a loop construct is equal to E E . This denotes that a loop may not be accessed if the condition b does not hold, hence the initial environment remains unchanged.
Static Security Checks
We present in Figure 5 the static security checks performed by our analysis before using a pointer of type τ = ref ρ (κ) η . Some of these checks refer to the effects model σ to verify the presence or the absence of a specific effect. We define the function oneTrace(µ, σ) that returns true, if the effect µ is present in at least one possible trace extracted from the effect model σ.
Figure 5. Static security checks for memory access
Safe Pointer Dereference. The safeRead(e, τ, σ, ) checks that pointer e of type τ can be safely dereferenced at program point It fails for void, freed, unallocated, and NULL pointers. Statically, we consider dereference of arithmetic pointers as unsafe. We issue an error for accessing such pointers. However, we plan to resort to dynamic analysis to verify pointer boundaries as described in Section 6. Safe Assignment. The safeWrite(e, τ, τ , ) checks that the rhs expression e of type τ can be assigned to an lvalue of type τ . It fails if the rhs expression is uninitialized or if it has a declared type different from the lvalue. Safe Memory Deallocation. The safeFree(l v , τ, σ, ) checks that pointer l v can safely be deallocated at program point . It fails for un-allocated, freed, and not dynamically allocated pointers. For the last case, we use the collected effects model σ to verify that the region to free has previously been allocated. In other words, we verify that an effect alloc(ρ, _) is present in the effects trace σ of the program before freeing region ρ.
Static Analysis Limitations
As for all static techniques, our conservative type analysis generates false positives and has undecidability issues when runtime information is required. In fact, our static approach has limitations as detailed in the following cases:
• We may face undecidability when static security checks are performed on a may-aliased expression that has two possible types depending on the chosen execution path. Since we can not statically determine the executed branch, we require both types τ 1 and τ 2 in a given type construct if (τ 1 , τ 2 ) to be safe in order to pass the security check. If one of the types succeeds and the other fails, we face an undecidable case and the check fails.
• Our analysis performs an exhaustive traversal of all execution paths of the program. However, the analysis is path-insensitive and does not prune infeasible paths. Hence, we may generate false positives by considering paths that actually are never executed.
In a future work, we plan to reduce the number of false positives and solve undecidable cases by resorting to code instrumentation. The generated effects model is useful to guide the instrumentation of the code, for it captures the suspected memory operations, their program point, and their execution paths.
Inference Algorithm
This section is dedicated to region, effect, and host annotations inference. The algorithm Infer is applied recursively on expressions and statements to evaluate their types and annotations. The complete algorithm Infer algorithm is presented in Figure 6 . For expressions, the Infer algorithm takes as input a type environment E, an expression e, and its program point . It returns a type for the expression and a generated effect from the evaluation of the expression. For statements, the algorithm takes as input the current environment E, a statement s, and its program point . The evaluation of statement s yields a new type environment E computed by the updEnv() algorithm and a generated effect. The inference algorithm fails if the static security checks defined in Section 5 for memory safety fail.
Soundness
In the following, the intention is to prove that our inference algorithm is sound with respect to the static semantics.
Soundness (Theorem) Let E be the typing environment, e an expression, and s a statement:
• If Infer(E, , e) = (τ, σ) , then E , e : τ, σ.
•
Proof of Soundness The proof is done by structural induction on expressions. Due to space constraints, we present a sketch of the proof for the (ref) rule and the (assign) rule:
Figure 6. Annotations inference algorithm
• Case of (pointer deref): By hypothesis, we have
Infer(E, , * e) = (τ, (σ; read(r, τ, ))).
By the definition of the algorithm, this requires:
and safeRead(e, τ, σ, ) and storedType(τ ) = τ
By the definition of the (pointer deref) rule, we have:
• Case of (assign): By hypothesis, we have
By the definition of the algorithm, this requires:
Infer(E, , lv) = (τ, σ) and Infer(E, , e) = (τ , σ ) and safeWrite(e, τ , τ, ) and r = regionof (lv) and E = updEnv(E, lv = e, )
By the definition of the (assign) rule, we have:
Implementation and Case Study
We prototyped our approach as an extension to the GCC compiler for the C programming language [8] . Our implementation is based on the GCC core distribution version Figure 7 illustrates our implementation of the type analysis. The output of our static pass shows that we can detect errors and outputs their execution traces based on the collected effects. Furthermore, our analysis can detect undecidable cases when dealing with branch conditions such as in line 18 of the sample code. It also outputs the exact trace that can lead to a double free of pointer buf1. Hence, we show that our approach can be easily extended in a future work to cooperate with a dynamic analysis in order to reduce false positives and solve undecidable cases.
Related Work
This section presents approaches and tools for vulnerabilities detection in C source code. The MetaCompilation (MC) [1] is a static analysis tool that uses a flow-based analysis approach for detecting temporal security errors in C code. Their analysis is flow-sensitive, however unlike our approach they do not perform alias analysis and rely on heuristics to deal with aliasing issues. MOPS [4] is another tool that detects temporal vulnerabilities using a modelchecking technique. MOPS is more appropriate to detect high-level security properties than safety properties. In fact, it assumes that the analyzed program is memory safe. There are some others model-checking tools based on predicate abstraction for vulnerabilities detection in source code such as BLAST [14] , and SLAM [3] . The SLAM model checker is mainly used to verify windows drivers and have not been used for verifying memory and type errors. The BLAST model checker does not easily handle C pointers, it has been used with CCured to reduce runtime checks for memory errors.
Type systems have been used to verify security properties in source code. The type-based approach used by the tool CQual [7] , consists of extending the type system with type qualifiers that are used to express security properties. To our knowledge, it has not been used to detect memory and type errors as we do. The literature contains proposals on hybrid approach analysis that combines static and dynamic analysis: CCured [9] , SafeC [2] , Vault [6] , and Cyclone [10] . These language-based tools extend the C type system in order to detect memory and type errors. They resort to code instrumentation when static analysis undecidability is faced. We still did not define a dynamic phase for our approach. However we illustrated that the effects model that we generate can be extended in future work to guide code instrumentation.
Conclusion
We presented a novel flow-sensitive type and effect analysis for detecting memory errors in C source code. Our type analysis is based on effect, region, and host annotations. We defined security checks that are compliant with the ANSI-C standard, we do not allow operations forbidden by the standard. However, we added restrictions to ensure memory safety not supported by the standard C type system. We developed a flow-sensitive inference algorithm to insert annotated types to program. The advantage of our algorithm is that annotations are automatically inferred without any external intervention. Furthermore, the flowsensitivity and alias analysis of our inference algorithm enabled us to detect more efficiently temporal memory errors and to address C aliasing pitfalls. Our approach based on effects analysis can also be easily extended with runtime checks to increase its precision and reduce the number of false positives.

{'paper_id': '731404', 'title': 'Type and Effect Annotations for Safe Memory Access in C', 's2_url': 'https://api.semanticscholar.org/CorpusID:731404', 'source': 'S2ORC'}