[ANN] Mopsa 1.0 -- Modular Open Platform for Static Analysis

Community
1

Dear all,

On behalf of all its developers, I am glad to announce the release of Mopsa 1.0! You can just opam install mopsa.

Mopsa stands for Modular and Open Platform for Static Analysis. It aims at easing the development and use of static analyzers. More specifically, Mopsa is a generic framework for building sound static analyzer based on the theory of abstract interpretation. Mopsa is independent of language and abstraction choices. Developers are free to add arbitrary abstractions (numeric, pointer, memory, etc.) and syntax iterators for new languages. Mopsa encourages the development of independent abstractions which can cooperate or be combined to improve precision.

Mopsa currently support the analysis of Python, C and Python+C programs. It reports run-time errors on C programs and uncaught exceptions on Python programs. Our benchmarks provide an illustrative overview of what Mopsa can currently analyze. All analyses currently provided are flow and context-sensitive (i.e, control-flow operators are taken into account by the analysis, and functions are analyzed by virtual inlining). The C analysis is actively developed and maintained. The Python and Python+C analyses work on real-world examples, but are not actively developed.

Please note that Mopsa is an academic tool under development. Feel free to submit issues if you encounter any bug!

Additional resources:

15 Likes
2

As a professional python developer I am pretty interested in your static analysis features in that space. What is the main differentiating factor compared to say, ruff, mypy, etc.?

It sounds more extensible and thus offers richer analysis in the long run?

Thanks

3

I took a quick look at MOPSA, and I was able to start analyzing some of the OCaml 4.14 code with it (after mopsa-build: handle -Wl,-E correctly (!234) · Merge requests · MOPSA / MOPSA analyzer · GitLab).
(I also tried OCaml 5, but it doesn’t yet support the C atomics needed by it)

The abstract debugger is quite neat, for example:

mopsa-c mopsa.db -make-target=ocamlyacc -c-check-signed-arithmetic-overflow=false -c-check-signed-implicit-cast-overflow=false -c-check-unsigned-implicit-cast-overflow=false -engine=interactive -config=c/cell-string-length-pointer-sentinel-pack-rel-itv-congr.json

This seems like a valid complaint, if myname is NULL we shouldn’t attempt to use it as a %s argument:

 280:  * requires: valid_string_or_fail(s);
                    ^^^^^^^^^^^^^^^^^^^^^^^ 
  NULL pointer dereference
  Callstack:
        from ./yacc/error.c:34.4-53: _mopsa_assert_valid_string
        from ./yacc/main.c:162.17-27: no_space
        from ./yacc/main.c:426.4-23: getargs
        from ./yacc/main.c:423.4-11: main


/var/home/edwin/.opam/5.2.0+fp/share/mopsa/stubs/c/mopsa/mopsa.c:280.13-36
   275   */
   276  void _mopsa_assert_valid_bytes(void *p, _mopsa_size_t n);
   277  
   278  /*$
   279  
 ► 280   * requires: valid_string_or_fail(s);
   281   */
   282  void _mopsa_assert_valid_string(char *s);
   283  
   284  /*$
   285   * requires: valid_substring(s,n);
𝕊 ⟦ requires ((((((s != (void *) 0) otherwise raise("NULL pointer dereference")) and ((s != INVALID) otherwise raise("Invalid pointer dereference"))) and (alive(s) otherwise (resource(s) ? raise("Use after free") : raise("Dangling pointer dereference")))) and (((offset(s) >= 0) and (bytes(s) >= (offset(s) + 1))) otherwise raise("Out-of-bound access"))) and (∃_i ∈ [0 .. ((bytes(s) - offset(s)) - 1)] : (s[_i] == 0) otherwise raise("Non-terminating string"))); ⟧
mopsa >> back 
./yacc/error.c:34.4-53
   29  }
   30  
   31  
   32  void no_space(void)
   33  {
 ► 34      fprintf(stderr, "%s: f - out of space\n", myname);
   35      done(2);
   36  }
   37  
   38  
   39  void open_error(char_os *filename)
𝔼 ⟦ _mopsa_assert_valid_string(myname) : void ⟧
mopsa >>  
./yacc/main.c:162.17-27
   157  {
   158      register int i;
   159      register char_os *s;
   160  
   161      if (argc > 0) myname = caml_stat_strdup_of_os(argv[0]);
 ► 162      if (!myname) no_space();

You can also analyze ocamlrund (but not ocamlrun because that uses the unsupported AddrLabelExpr in jumptbl.h).

5 Likes
4

Thank you for your interest! One of the goals of Mopsa is to explore the design of new analyses. As such, we target analyses that are sound, and more precise than mypy’s. We aim to design sound analyses, meaning we take into account all behaviors of a program – which in the case of Python’s semantics can quickly be expensive. Regarding precision, we have analyses able to infer Python types, or track the length of lists for example. This however comes at the cost of less scalability, and the ability to analyze functions only when a given calling context is provided (i.e, analyzing Python libraries in isolation is currently not possible).

Mopsa is a research project, and I don’t think the Python analyses are stable enough to analyze arbitrary code and be used in production yet.

1 Like