New Webpage
MOPSA has a new Webpage
Version 1.0 of MOPSA is released! Read more
MOPSA
MOPSA - A Modular Open Platform for Static Analysis is a research-oriented platform written in OCaml to build sound semantic static analyzers based on Abstract Interpretation.
Our goal with MOPSA is to encourage the research and education in Abstract Interpretation by providing a fully-featured and extensible open-source platform and usable analyses built with it.
Features
MOPSA is a research project providing a unique platform for static analysis
Automated Source Analysis
MOPSA analyses source code without executing it and reports alarms for possible errors, such as arithmetic or pointer errors in C or uncaught exceptions in Python.
Sound & Semantic
Based on the Abstract Interpretation theory, MOPSA computes an abstract model of your program’s executions. It is sound by design, covering all cases, but can report false alarms.
Abstract Debugger
MOPSA features a unique interactive abstract debugger to run your analysis step-by-step and understand the cause of imprecisions or soundness issues.
Extensible Platform
MOPSA has a modular architecture: an analysis is composed of several collaborating abstractions. It is easy to add more.
Multi-Language Support
MOPSA currently supports a large subset of C and Python 3, with more languages to come. It can even analyze programs mixing C and Python!
Transparent Results
MOPSA describes which properties hold safely according to its analysis, as well as any soundness assumptions it used to analyze the program.
MOPSA is a research project. 🔬
While it performs well on realistic benchmarks (e.g., Coreutils programs) and in the SV-COMP 2024 academic competition, it may not analyze arbitrary C or Python code, and may not be ready yet for production!
We are open to academic and industrial collaborations, feel free to get in touch!
If you have questions, please use our issue tracker.
Latest News!
MOPSA 1.0 released!
Version 1.0 of MOPSA is released and available as an Opam package.
Gold Medal 🥇 for the Software System category at SV-COMP 2024
MOPSA won the Gold Medal in the Software System category for its second participation to the SV-COMP software verification competition.
Source Code Analysis 🔎
MOPSA works fully automatically on the source code, without executing it. Unlike most linters, SAST tools and compiler-integrated analyses, MOPSA performs an in-depth, flow-sensitive, context-sensitive, field-sensitive, relational, and disjunctive analysis (yes, it can be slower).
MOPSA reports alarms for possible errors such as arithmetic or pointer errors in C or uncaught exceptions in Python.
MOPSA requires the full source code in order to build a faithful model of your program. It comes with a large subset of the C standard library already modeled for you.
You can try MOPSA now by installing our Opam package: just type opam install mopsa, or click below for more installation options:
Sound Semantic Analysis 🧮
MOPSA is based on the theory of Abstract Interpretation, pioneered by Radhia Cousot and Patrick Cousot.
Starting from a formal, mathematical semantics that faithfully models the programming language, MOPSA automatically computes an abstract model of your program’s executions.
MOPSA is sound by design, covering all (even unlikely) cases allowed by the semantics. To remain scalable without sacrificing soundness, MOPSA performs conservative approximations that may result in false alarms.
Modular Abstractions 🧩
MOPSA has a modular architecture: Each analysis is built on a constellation of small abstract domains that focus on a single program construction or data abstraction each and collaborated together with low coupling.
Domains can be easily swapped in and out, and combined through reduced products.
The small granularity of abstract domains is a unique feature of MOPSA. It also relies on a novel framework for dynamic expression rewriting to help domains collaborate to analyze complex statements.
MOPSA comes ready with several choices of abstractions for C and Python analysis, but it is easy to add more!
Multi-Languages 🌐
MOPSA is built to support any programming language. Version 1.0 supports large subsets of C and Python 3, with support for more languages being developed in our research projects. MOPSA can even analyze projects mixing C and Python!
MOPSA works as an interpreter on a high-level representation of programs: Abstract Syntax Trees. Unlike most analyzers, MOPSA does not require a low-level representation of programs, instead relying on its dynamic expression translation engine to handle complex statements.
It is easy to add new AST nodes and the abstract domains to handle them.
Research-Oriented 🧪
Our goal: Encourage the research and education in static analysis by abstract interpretation and the formal verification of software. MOPSA is open-sourced on a LGPL 3 license, for everyone to modify.
For education, MOPSA includes a toy-language that uses the same framework and basic abstractions, but is easier to grasp and tinker with than full C.
For research, MOPSA provides ready to use C and Python analyses, core abstractions, library support that you can build upon to accelerate your development and experiment quickly on realistic programs. MOPSA provides developer tools, such as logs and hooks, to instrument analyses and understand the causes of imprecision and unsoundness. MOPSA features a unique interactive abstract debugger to run your analysis step-by-step.
Support & Funding 🏫
MOPSA developers are researchers, PhD, post-docs and interns supported by their host institutions (Sorbonne Université, École Normale Supérieure, CNRS, Inria).
MOPSA started as an ERC Consolidator Grant (2016-2021) awarded to Antoine Miné.
Since then, MOPSA has been funded by several French and European research grants:
- SecurEval Project from PEPR Cybersécurité program, PI: Antoine Miné
- SWHSec Project from PTCC program, PI: Antoine Miné
- AVoCat Project (2023-2027) from Inria Exploratory Action program, PIs: Raphaël Monat and Aymeric Fromherz
- RAISIN Project (2024-2028) from ANR “JCJC” program, PI: Raphaël Monat