-{"header":"<h1 id=\"the-codex-static-analysis-library\"><a href=\"#the-codex-static-analysis-library\" class=\"anchor\"></a>The Codex static analysis library</h1>","type":"documentation","uses_katex":true,"breadcrumbs":[{"name":"Index","href":"../index.html","kind":"leaf-page"},{"name":"codex","href":"#","kind":"page"}],"toc":[{"title":"Analyzers","href":"#analysers","children":[]},{"title":"Core static analysis modules","href":"#core-static-analysis-modules","children":[]},{"title":"Optional static analysis modules","href":"#optional-static-analysis-modules","children":[]},{"title":"Utilities","href":"#utilities","children":[]},{"title":"Tutorials","href":"#tutorials","children":[{"title":"Extending Codex to a simple while language","href":"#extending-codex-to-a-simple-while-language","children":[]},{"title":"Using the Codex type system for C and binary analysis","href":"#using-the-codex-type-system-for-c-and-binary-analysis","children":[]}]}],"source_anchor":null,"preamble":"<p>Codex is a library of reusable components that are needed to implement a new static analyzer. The main component of any static analysis based on abstract interpretation are:</p><ul><li><a href=\"Single_value_abstraction/index.html\"><code>Single_value_abstraction</code></a> which abstract unbounded integers <code class=\"odoc-katex-math\">\\mathbb Z</code>, fixed sized bitvectors (of any arbitrary size), and booleans (<a href=\"Lattices/Quadrivalent/index.html\"><code>Lattices.Quadrivalent</code></a>);</li><li>Abstract <a href=\"Domains/index.html\"><code>Domains</code></a>, that perform the basic analysis operations. In the case of non-relational domains, domains are built using <a href=\"Single_value_abstraction/index.html\"><code>Single_value_abstraction</code></a>.</li><li>A <a href=\"Fixpoint/index.html\"><code>Fixpoint</code></a> engine, that iterates analysis operations until everything was computed;</li><li>A frontend, that parses the source code and drive the analysis by calling the <a href=\"Fixpoint/index.html\"><code>Fixpoint</code></a> engine and translating instructions and expressions to <a href=\"Domains/index.html\"><code>Domains</code></a> operations. This depends on the language to be analyzed, so this is not provided by the Codex library; but see <a href=\"#analysers\" title=\"analysers\">Analyzers</a> for analyzers that use the library.</li></ul><p>The Codex repository is decomposed in several sub-parts (that are in different directories), whose dependency graph is as follows: <img src=\"../../../dependency_graph.png\" alt=\"Dependencies between Codex modules\" /></p>","content":"<h2 id=\"analysers\"><a href=\"#analysers\" class=\"anchor\"></a>Analyzers</h2><p>Each analyzer must set up its stack of abstract domain, then translate the analysis of instructions and expressions in calls to abstract domains. See for instance:</p><ul><li><a href=\"../frama_c_codex/index.html\">Frama-C/Codex</a>: C code analysis implemented as a Codex-based Frama-C plugin. There, check <a href=\"../frama_c_codex/Core/Codex_register/index.html\">Codex_register</a> which builds the stack of domain (that you can also observe dynamically using <a href=\"Tracelog/index.html\"><code>Tracelog</code></a>), and <a href=\"../frama_c_codex/Core/C2Codex/index.html\">C2Codex</a> which interprets the C AST using the <a href=\"Operator/index.html\"><code>Operator</code></a> implemented inside the abstract <a href=\"Domains/index.html\"><code>Domains</code></a>.</li><li><a href=\"../binsec_codex/index.html\">BINSEC/Codex</a>: Binary code analysis implemented as a Codex-based BINSEC plugin. There, the <a href=\"../binsec_codex/Binsec_codex_lib/Dba2Codex/index.html\">Dba2Codex</a> module which instantiates a stack of <a href=\"Domains/index.html\"><code>Domains</code></a>, and handles the translation form BINSEC's DBA intermediate language to Codex <a href=\"Operator/index.html\"><code>Operator</code></a>.</li><li>(Upcoming) While analyzer and other examples.</li></ul><p>Note that using <a href=\"Tracelog/index.html\"><code>Tracelog</code></a> you can observe the recursive calls to the different domains, i.e. trace how the analysis of a source expression is handled by Codex.</p><h2 id=\"core-static-analysis-modules\"><a href=\"#core-static-analysis-modules\" class=\"anchor\"></a>Core static analysis modules</h2><ul><li><a href=\"Operator/index.html\"><code>Operator</code></a> : Definition of the concrete semantics of base objects like booleans, integers, bitvectors; and utilities around them (like function symbols).</li><li><a href=\"Lattices/index.html\"><code>Lattices</code></a> : Abstraction of a set; lattices representing abstraction of a single value the main way to exchange information in Codex.</li><li><a href=\"Single_value_abstraction/index.html\"><code>Single_value_abstraction</code></a> : Combination of <a href=\"Lattices/index.html\"><code>Lattices</code></a> abstracting a single value by <a href=\"Operator/index.html\"><code>Operator</code></a>.</li><li><a href=\"Terms/index.html\"><code>Terms</code></a> : is the symbolic terms that is the target of our SSA-translation by abstract interpretation.</li><li><a href=\"Types/index.html\"><code>Types</code></a> : AST and parser used by the type-based analysis.</li><li><a href=\"Domains/index.html\"><code>Domains</code></a> : The SSA/value-based domains, as well as the memory domains.</li></ul><h2 id=\"optional-static-analysis-modules\"><a href=\"#optional-static-analysis-modules\" class=\"anchor\"></a>Optional static analysis modules</h2><ul><li><a href=\"Fixpoint/index.html\"><code>Fixpoint</code></a> : A library that helps perform fixpoint computation.</li><li><a href=\"Smtbackend/index.html\"><code>Smtbackend</code></a> : Operates a translation of Terms to an SMT formula.</li></ul><h2 id=\"utilities\"><a href=\"#utilities\" class=\"anchor\"></a>Utilities</h2><ul><li><a href=\"Codex_config/index.html\"><code>Codex_config</code></a> : Contains knobs allowing to change the behavior of some abstract domains. We generally avoid doing this, but it is useful for benchmarking.</li><li><a href=\"Tracelog/index.html\"><code>Tracelog</code></a> The logger. Instantiate it on top of your module, then use <code>Log.debug(fun p -> p ...)</code> where p behaves like <code>Format.printf</code>.</li><li><a href=\"../patricia-tree/PatriciaTree/index.html\"><code>PatriciaTree</code></a> : Now a stand-alone submodule, but works specially well for abstract interpretation purposes.</li><li><a href=\"Codex_log/index.html\"><code>Codex_log</code></a> is the old, deprecated, logger.</li></ul><h2 id=\"tutorials\"><a href=\"#tutorials\" class=\"anchor\"></a>Tutorials</h2><h3 id=\"extending-codex-to-a-simple-while-language\"><a href=\"#extending-codex-to-a-simple-while-language\" class=\"anchor\"></a>Extending Codex to a simple while language</h3><p>We present a tutorial on a simple imperative <code>while</code> language, and demonstrates how to statically analyze programs written in it using Codex, a modular abstract interpretation library. This also serves as a nice introduction to various codex components (<a href=\"Lattices/index.html\"><code>Lattices</code></a>, <a href=\"Single_value_abstraction/index.html\"><code>Single_value_abstraction</code></a>, <a href=\"Domains/index.html\"><code>Domains</code></a>...). It is mostly meant for developers who wish to use and extend Codex.</p><ul><li><a href=\"While tutorial - chapter 1.html\" title=\"While tutorial - chapter 1\">Chapter 1</a>: Contains the syntax which is defined with variables, arithmetic, boolean expressions, and control structures (e.g., <code>if</code> and <code>while</code>). It also provides a concrete interpreter for the <code>while</code> language;</li><li><a href=\"While tutorial - chapter 2.html\" title=\"While tutorial - chapter 2\">Chapter 2</a>: Describes <a href=\"Lattices/index.html\"><code>Lattices</code></a> and <a href=\"Single_value_abstraction/index.html\"><code>Single_value_abstraction</code></a> with simpler implementations;</li><li><a href=\"While tutorial - chapter 3.html\" title=\"While tutorial - chapter 3\">Chapter 3</a>: Contains simple interval abstract domain which is then used to run the analysis on simple while programs;</li><li><a href=\"While tutorial - chapter 4.html\" title=\"While tutorial - chapter 4\">Chapter 4</a>: Shows how one can use Codex building blocks to recreate the interval domain from chapter 3.</li></ul><h3 id=\"using-the-codex-type-system-for-c-and-binary-analysis\"><a href=\"#using-the-codex-type-system-for-c-and-binary-analysis\" class=\"anchor\"></a>Using the Codex type system for C and binary analysis</h3><p><a href=\"Types tutorial.html\" title=\"Types tutorial\">This tutorial</a> provides a user guide for the static analysis based on the dependent nominal type system presented in the <a href=\"https://codex.top/papers/2024-oopsla-typedc-dependent-nominal-physical-type-system.html\">OOPLSA 2024 paper</a> and implemented using Codex. It covers all the steps necessary to use our tool to check if a C or machine code program is exempt of spatial memory safety errors, such as null pointer dereferences, buffer overflows, or type confusion errors. It covers in particular:</p><ul><li>How to run the analysis on a C program, how to configure the C analysis, and how to inspect the results.</li><li>How to run the analysis on a binary executable, how to configure the machine code analysis, and how to inspect the results.</li><li>How to specify the types used in a C programs to refine the results of the analysis (which is generally a necessary step to obtain memory safety).</li></ul>"}
0 commit comments