Coccinelle is a program matching and transformation engine which provides the language SmPL (Semantic Patch Language) for specifying desired matches and transformations in C code.

Coccinelle is a tool for pattern matching and text transformation that has many uses in kernel development, including the application of complex, tree-wide patches and detection of problematic programming patterns.

Installation

The most convenient way i found to install Coccinelle is through OCaml package manager, aka Opam.

So, first, install Opam

pacman -S opam #For Arch distros

apt-get install opam #For Debian-like distros

and then Coccinelle with the following commands

opam update
opam install coccinelle

The source code of Coccinelle can also be found on Github.

SmPL Sintax

Coccinelle is based on Semantic Patch sintax which re-creates patterns of C language. Coccinelle uses this sintax to create the rules to parse the actual code.

For the most part, the grammar is written using standard notation. In some rules, however, the left-hand side is in all uppercase letters. These are macros, which take one or more grammar rule right-hand-sides as arguments. The grammar also uses some unspecified nonterminals, such as id, const, etc. These refer to the sets suggested by the name, i.e., id refers to the set of possible C-language identifiers, while const refers to the set of possible C-language constants.

A square bracket that is surrounded by spaces in the description of a term should appear explicitly in the term, as in an array reference. On the other hand, square brackets that surround some other term indicate that the presence of that term is optional.

An example of SmPL sintax:

@@ expression E; constant C; @@
(
  !E & !C
|
- !E & C
+ !(E & C)
)

More information about the SmPL grammar can be found in the official documentation.

How to use it

Coccinelle can be used as static analysis tool on any C-based project but, for now, consider the Linux Kernel code.

In order to use Coccinelle, download the Linux Kernel source code and apply a Coccinelle script to it.

$ cd linux_mainline
$ spatch --sp-file script.cocci

or selecting a target folder to analyse:

$ spatch --sp-file script.cocci --dir drivers/

For a later analysis, it’s useful to save logs on a file:

$ spatch --sp-file script.cocci --dir drivers/ 2>&1 | tee log.txt

A list of examples of Coccinelle rules, and related .cocci files, are available here https://coccinelle.gitlabpages.inria.fr/website/rules.

Coccinelle for Rust

As the Linux kernel, and systems software more generally, is starting to adopt Rust, there is a version of Coccinelle for Rust, to make the power of Coccinelle available to Rust codebases.

The source code of Coccinelle for Rust is available here: https://gitlab.inria.fr/coccinelle/coccinelleforrust.

It relies on Rust Analyzer for parsing and rustfmt for pretty printing. It mainly supports matching and transformation of expressions and types, but reasoning about control flow is not yet supported. In fact, Coccinelle for Rust is currently a prototype and under heavy development to add features and improve use-cases.

Considerations

Some of the rules used for stardard Coccinelle for C projects, such as “Dereferences of NULL pointers”, “Dereferences of invalid pointers”, “Resource allocation” becomes useless in Rust since the compiler already checks that.

While most memory vulnerabilities are eliminated by the rustc compiler, there seem to be two main types of bugs in that could potentially be present in the linux kernel:

  1. Unsafe blocks: they bypass all types of security enforced by the rust compiler but, probably, the number of remaining issues would be dramatically less compared to C because unsafe blocks has to be accompanied by a block of safety documentation.

  2. Rust-C integration: probably the main source of bugs/issues would be found at the interface of Rust