xref: /src/doc/roadmaps/verification

$NetBSD: verification,v 1.1 2017/01/13 10:14:58 dholland Exp $

NetBSD Verification Roadmap
===========================

This roadmap covers things that we intend or would like to do pursuant
to verification and quality control.

The following elements, projects, and goals are relatively near-term:

 1. Cut down the Coverity backlog
 2. Deploy asan/ubsan
 3. Deploy clang-static-analyzer

The following elements, projects, and goals are longer-term:

 4. mint
 5. Database-driven program analyzer

The following elements, projects, and goals are rather blue-sky so far:

 6. Use Frama-C to verify fsck_ffs


Explanations
============

1. Cut down the Coverity backlog

Coverity provides us with free analysis reports, which we sometimes
handle and sometimes don't. Apparently though Linux has a lower number
of Coverity hits per line than we do; that seems fundamentally wrong
and something that should get attention. Most of the problems Coverity
finds are pretty easily fixed, or are false positives.

 - As of January 2017 coypu has been working on this. Christos often
   also fixes these.
 - There is currently no clear timeframe or release target.
 - Contact christos for further information.


2. Deploy asan/ubsan

It ought to be possible to build any program in NetBSD, or the whole
world, using asan and/or ubsan. Currently there isn't an easy way to
do this. We should also do regular test runs with asan and ubsan
engaged.

 - As of January 2017 nobody is known to be working on this.
 - There is currently no clear timeframe or release target.
 - Contact joerg (?) for further information.


3. Deploy clang-static-analyzer

There is some makefile support for running clang-static-analyzer, but
it doesn't get done regularly. This should probably get added to the
autobuilds.

 - As of January 2017 nobody is known to be working on this.
 - There is currently no clear timeframe or release target.
 - Contact joerg for further information.


4. mint

A while back dholland started on a replacement for the existing lint,
since lint is not really smart enough to be useful and its code is
only marginally maintainable. The code is in othersrc, but it needs
some tidying before anyone else tries hacking on it.

 - As of January 2017 nobody is known to be working on this.
 - There is currently no clear timeframe or release target.
 - Responsible: dholland


5. Database-driven program analyzer

In the long run we would like to have a program analyzer that can
scale to the whole kernel and can do differential analyses across
different versions. This is a nontrivial project though.

 - As of January 2017 nobody is known to be working on this.
 - There is currently no clear timeframe or release target.
 - Contact: dholland


6. Use Frama-C to verify fsck_ffs

Frama-C is a framework for doing formal verification of C code using
(mostly) precondition/postcondition specs. It is not everything one
necessarily wants in a verification framework; but on the other hand
it exists and people do use it.

fsck_ffs seems like a good candidate for this because it's
mission-critical and what it needs to do is comparatively well
understood even in detail. However, the code may be too messy.

 - As of January 2017 nobody is known to be working on this.
 - There is currently no clear timeframe or release target.
 - Contact: dholland