Static verification is formally, the verification of a set of given properties over a program’s semantics. Such semantics can be determined before compilation, and are typically modeled as mathematically provable properties. Dynamic verification on the other-hand, while not verifying static semantics, verifies desired properties during execution. This often requires extensive suites of test cases. In mission critical software applications, greater certainty in software correctness is needed.

Background

Memory errors

Memory errors are critical issues in software development. We distinguish them into two categories. First are spatial memory errors which concern mismanagement of the space which memory occupies. For example, accesses to memory outside its allocated boundaries. Temporal errors arise when memory is accessed after it has been released, resulting in unpredictable behavior. This chiefly includes use-after-free memory errors and similarly dangling references. Dangling pointers are pointers to memory that have been deallocated or freed. An attempted access or modification to the underlying memory is called a use-after-free. The detection of memory errors is of vital importance to software security, especially in mission critical software applications. However, enforcing memory safety proves to be difficult [1]. Across the literature, operations on memory are broken into four types:

Software analysis

Variations of software analysis are summarised briefly below.

Literature survey

Formal methods of software verification

Denotational semantics for data-dependence

In the absence of runtime information regarding data-dependence relations, we can represent a program via statements and expressions that denote the program’s actual semantics. This forms the basis of denotational semantics. In 1996, Ge et al’s "Effective Representation of Aliases and Indirect Memory Operations in SSA Form" formulated a denotational semantics for data-dependence relations [5].

Notably, this extends to address-taken or "indirect" variables. SSA form will be discussed later. However, this representation of data-dependence relations is crucial for abstractly representing program semantics pertaining to memory operations.

Abstract interpretation

Given a program’s semantics, formal methods can be applied to prove properties true mathematically. In "A Unified Approach to Global Program Optimization" [6], G.A Kildall formalised such a method as a lattice of data-flow semantics. Shown below is an example of a lattice of 3 program variables. Elements of the lattice are ordered by semantic detail, that is, by the accuracy of statements regarding a program’s dataflow, at particular points in execution. Then, the determination of a program’s semantics is the maximal fixed-point (MFP) in the lattice; determined via recursive application of the "meet" operation (denoted ∧). Kildall demonstrated that this algorithm can decidably obtain the MFP. Subsequently, Kam and Ullman demonstrated that, for a less constrained set of problems, the meet-over-all paths (MOP) solution—an approximation of the MFP becomes decidable [7]. This decidability is achieved by restricting the set of operations to monotonic ones. In the following discussion, we delve into a crucial analysis situated within this monotonic framework.

Pointer analysis

Static pointer analysis is foundational to software verification. L.A. Andersen introduced a monotonic framework for deciding the points-to set of program variables. The points-to set is the set of all program variables and memory objects a particular pointer may point to during execution. Modeled as a constraint satisfaction problem [8], monotonicity [9] ensures that we arrive at an accurate determination of points-to information of program variables.

However, Andersen’s pointer analysis (APA) is constrained to a cubic time complexity [9] with respect to the number of program variables, or equivalently, the number of nodes in the dataflow diagram. Appropriately, there exists an abundance of techniques to approximate the points-to information via the reduction of the node count at minimal cost to accuracy. Most notable is demand-driven pointer analysis which seeks to apply APA to the most relevant subset of nodes given specific user queries [10]. Cycle reduction, the removal of cyclical pointer relationships, proves to be highly effective [11]. Sui et al’s Supa employs demand driven pointer analysis on sparse value-flow diagrams [12] to great effect.

Variable substitution, the symbolic grouping of highly dependent variables, generate a 54% reduction in analysis time [13]. Augmentations of existing constraint graph structures provide further node reduction. Considering sparsity, which notionally considers the locality of memory, can be employed to provide precision preserving pointer analyses over a reduced node count [14]. The tool Pus provided a 7 times increase in running time when employing sparsity constraints [14].

Many of the optimisations mentioned are available to us through the SVF framework. In terms of pointer analysis, SVF is utilised to provide a optimised constraint graph [16] data structure [17].

Software correctness and verification

We will first consider the boolean satisfiability problem (SAT), that being the problem of determining if, for a boolean expression of variables, a set of assignments makes the expression evaluate to true. In 1971, Cook [18] proved that SAT is NP-Complete. Thus, it generally regarded as an undecidable problem. Furthermore, it is unlikely that a polynomial time algorithm exists that can solve SAT problems in general. This indicates a large problem for software verification whereby we must, equivalently, satisfy a set of properties of our program’s semantics. For any productivity in this domain, we must turn to heuristic and approximate methods. We first consider below the subset of SAT problems, CNF-SAT. Since boolean expressions in disjunctive normal form are trivially, polynomial-time verifiable (via short-circuiting), the primary bottleneck in developing tractable SAT solvers is in solving formulae in conjunctive normal form (CNF). This restriction to CNF-SAT becomes decidable, but not in polynomial time [19].

We are not directly concerned with SAT, rather an extension of SAT called satisfiablity modulo theories (SMT) which extends to theories besides Boolean algebra; notably, first-order logic, real numbers, and most relevant to us, program constraints. SMT is (polynomial time-) reducible to SAT [20], hence, it informs us greatly. Term rewriting, in regards to CNF-SAT can be applied as a technique of converting CNF-SAT problems into DNF-SAT problems, that can then be polynomial time decided. However, it is provably undecidable [21]. On the other hand, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm, developed in 1961 [22] decides CNF-SAT in exponential time [23]. It works via heuristically selecting (backtrack-able) boolean assignments recursively, and then among other boolean simplifications, applies term rewriting until a polynomial time satisfiable expression is found. Accompanying DPLL is DPLL(T), a framework that extends DPLL to SMT problems, or more specifically, any theory T . Its time complexity is dependent on the time complexity of translating the theory T into a SAT problem, for which DPLL can then solve. Adjacent to constraint programming [24] are theories of congruence closure which are O(n log n) time convertible to SAT [25].

In terms of memory safety verification, we aim to solve for theories of program variables, data structures, and memory objects as they appear in memory. Bjørner et al.’s "Satisfiability Modulo Bit-precise Theories for Program Exploration" [26] discusses efficient SMT solving for data-structures that are still accurate to their actual low-level representation in memory. z3 is a SMT solver developed by Microsoft Research. z3 makes use of the above methods to efficiently solve given propositions. However, there is a lack of optimisations that make use of memory information.

Approximate and domain specific approaches

Applicable to the pre-analysis stage are randomised approaches. Ge et al’s semantics seen above approximates the SMT solution space’s polytope vertices. On this basis, solution space vertices are greatly reduced in number. Albeit, this is applied to theories of linear arithmetic SMT(LA). In the same vein Xue et al’s "Under-Approximating Backward Reachable Sets by Polytopes" [28] approximates the backward-reachability sets within non-linear systems. This is equivalent to backwards-reachability when applied to a data-flow graph.

Similarly APA determines the program objects that given variables point to. APA is an example of a forward-reachability analysis.

Existing implementations

CBMC

CBMC, a bounded model checker for C and C++, solves programming constraints using a SAT solver. It identifies use-after-free memory errors in source code. In particular, it has translations for inbuilt operations as well as standard library functions into CNF-SAT boolean operations. Via term rewriting, it then produces a SAT problem that an external solver can satisfy. Vorobyov et al [30] finds that CBMC fails to compete with another use after free detection tool Parfait. Gui et al’s "Automated Use-After-Free Detection and Exploit Mitigation: How Far Have We Gone" [31] observers that CBMC fails to scale to larger software, despite having high precision.

SABER

Saber [31] detects memory leaks. It applies APA in a pre-analysis stage. Then, Saber constructs a sparse value flow graph (SVFG). The graph is annotated with "guards", or equivalently, memory constraints. These constraints are concrete implementations of the Chow et al. denotational semantics discussed earlier. Lastly, a reachability analysis is performed to determine the "sink" or deallocation site for all memory objects. These constraints are then encoded into a binary decision diagram (BDD) from which backwards-reachability is determined. A BDD is a tree like datastructure that represents a boolean function. This differs with an SMT approach. Nevertheless, it has the advantage in path redundancy elimination, which can be done efficiently on BDDs. Yan et al [32] have compared BDDs with sparse bitmaps, another datastructure commonly used in data-flow analysis; largely due to APA being "unification" based, fast set unions bode well for it. BDDs are shown to be faster and vastly more memory efficient because their memory usage grows with respect to the height of the BDD, not the node count.

Compared to SMT solvers, BDDs perform well within a subset of problems. Hardekop et al [33] comments on their viability in hardware, but notes that their limited support for higher-level program operations makes them less viable when used as a standalone solver. Furthermore, it is demonstrated that when used as an auxiliary datastructure to inform a later SMT solving stage, it is more efficient then using BDDs alone.

References

1. Santosh Nagarakatte, Milo and Zdancewic, S. (2015). Everything You Want to Know About Pointer-Based Checking. pp.190–208. doi:https://doi.org/10.4230/lipics.snapl.2015.190.
2. Yannis Smaragdakis, Bravenboer, M. and Ondřej Lhoták (2011). Pick your contexts well. Sigplan Notices, 46(1), pp.17–30. doi:https://doi.org/10.1145/1925844.1926390.
3. Alpern, B., Wegman, M.N. and Zadeck, F.K. (1988). Detecting equality of variables in programs. Proceedings of the 15th ACM SIGPLAN SIGACT symposium on Principles of programming languages - POPL ’88. doi:https://doi.org/10.1145/73560.73561.
4. Sui, Y., Ye, D. and Xue, J. (2014). Detecting Memory Leaks Statically with Full-Sparse Value-Flow Analysis. IEEE Transactions on Software Engineering, 40(2), pp.107–122. doi:https://doi.org/10.1109/tse.2014.2302311.
5. Chow, F., Chan, S., Liu, S.M., Lo, R., Streich, M. (1996). Effective representation of aliases and indirect memory operations in SSA form. In: Gyimóthy, T. (eds) Compiler Construction. CC 1996. Lecture Notes in Computer Science, vol 1060. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61053-7_66
6. Gary A. Kildall. 1973. A unified approach to global program optimization. In Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages (POPL ’73). Association for Computing Machinery, New York, NY, USA, 194–206. https://doi.org/10.1145/512927.512945
7. Kam, J.B., & Ullman, J.D. (1977). Monotone data flow analysis frameworks. Acta Informatica, 7, 305-317.
8. Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT SIGPLAN symposium on Principles of programming languages (POPL ’79). Association for Computing Machinery, New York, NY, USA, 269–282. https://doi.org/10.1145/567752.567778
9. Mathiasen, A.A. and Pavlogiannis, A. (2020). The Fine-Grained and Parallel Complexity of Andersen’s Pointer Analysis. arXiv.org. doi:https://doi.org/10.48550/arXiv.2006.01491.
10. Heintze, N., & Tardieu, O. (2001). Demand-driven pointer analysis. ACM-SIGPLAN Symposium on Programming Language Design and Implementation.
11. Rountev, A. and Chandra, S. (2000). Off-line variable substitution for scaling points-to analysis. ACM SIGPLAN Notices, 35(5), pp.47–56. doi:https://doi.org/10.1145/358438.349310.
12. Static Analysis. (2007). Lecture Notes in Computer Science. doi:https://doi.org/10.1007/978-3-540-74061-2.
13. Liu, P., Li, Y., Swain, B. and Huang, J. (2022). PUS: A Fast and Highly Efficient Solver for Inclusion-based Pointer Analysis. Analysis, 12. doi:https://doi.org/10.1145/3510003.3510075.
14. https://peimingliu.github.io/asset/pic/PUS.pdf
15. Barbar, M. and Sui, Y. (n.d.). Hash Consed Points-To Sets. Available at: https://yuleisui.github.io/publications/sas21.pdf.
16. Kodumal, J. and Aiken, A. (2004). The set constraint/CFL reachability connection in practice. ACM SIGPLAN Notices, 39(6), pp.207–218. doi:https://doi.org/10.1145/996893.996867.
17. GitHub. (n.d.). SVF/svf/include/Graphs/ConsG.h at master · SVF-tools/SVF. Available at: https://github.com/SVF-tools/SVF/blob/master/svf/include/Graphs/ConsG.h.
18. Cook, S.A. (1971). The complexity of theorem-proving procedures. Proceedings of the third annual ACM symposium on Theory of computing - STOC ’71. doi:https://doi.org/10.1145/800157.805047.
19. Bokov, G. (2018). Complexity of the CNF-satisfiability problem. Available at: https://arxiv.org/pdf/1804.02478.pdf
20. Biere, A., Heule, M. and Maaren, H. van (2009). Handbook of Satisfiability. [online] Google Books. IOS Press. Available at: https://www.google.com.au/books/edition/Handbook_of_S
21. Huet, G.P. (1978). On the Uniform Halting Problem for Term Rewriting Systems.
22. Davis, M. and Putnam, H. (1960). A Computing Procedure for Quantification Theory. Journal of the ACM, 7(3), pp.201–215. doi:https://doi.org/10.1145/321033.321034.
23. Ouyang, M. (1998). How good are branching rules in DPLL? Discrete Applied Mathematics, 89(1-3), pp.281–286. doi:https://doi.org/10.1016/s0166-218x(98)000456.
24. Selsam, D. and Leonardo de Moura (2016). Congruence Closure in Intensional Type Theory. Lecture Notes in Computer Science, pp.99–115. doi:https://doi.org/10.1007/9783-319-40229-1_8.
25. Harald Ganzinger, Hagen, G., Nieuwenhuis, R., Oliveras, A. and Tinelli, C. (2004). DPLL(T): Fast Decision Procedures. Lecture Notes in Computer Science, pp.175–188. doi:https://doi.org/10.1007/978-3-540-27813-914.
26. Bjørner, N., De Moura, L. and Tillmann, N. (n.d.). Satisfiability Modulo Bit-precise Theories for Program Exploration. Available at: https://leodemoura.github.io/files/smbpex.pdf
27. Ge, C., Ma, F., Zhang, P. and Zhang, J. (2018). Computing and estimating the volume of the solution space of SMT(LA) constraints. Theoretical Computer Science, 743, pp.110–129. doi:https://doi.org/10.1016/j.tcs.2016.10.019.
28. Xue, B., She, Z. and Easwaran, A. (n.d.). Under-Approximating Backward Reachable Sets by Polytopes. doi:https://doi.org/10.1007/978-3-319-41528-4.
29. Learning Interpretable Heuristics for WalkSAT, Yannet Interian, Sara Bernardini, University of San Francisco, Royal Holloway University of London
30. Vorobyov, Kostyantyn & Krishnan, Padmanabhan. (2010). Comparing Model Checking and Static Program Analysis: A Case Study in Error Detection Approaches.
31. Gui, Binfa Song, Wei Xiong, Hailong Huang, Jeff. (2021). Automated Use-After-Free Detection and Exploit Mitigation: How Far Have We Gone. IEEE Transactions on Software Engineering. PP. 1-1. 10.1109/TSE.2021.3121994.
32. H. Yan, Y. Sui, S. Chen and J. Xue, "Spatio-Temporal Context Reduction: A Pointer Analysis-Based Static Approach for Detecting Use-After-Free Vulnerabilities," 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE), Gothenburg, Sweden, 2018, pp. 327-337, doi: 10.1145/3180155.3180178.
33. Hardekopf, B. and Lin, C. (2009). Semi-sparse flow-sensitive pointer analysis. ACM SIGPLAN Notices, [online] 44(1), pp.226–238. doi:https://doi.org/10.1145/1594834.1480911.
34. Beyer, D. and Stahlbauer, A. (2014). BDD-based software verification. International Journal on Software Tools for Technology Transfer, 16(5), pp.507–518. doi:https://doi.org/10.1007/s10014-0334-1.
35. LLVM
36. https://github.com/nfinit/ansibench