Home | History | Annotate | Line # | Download | only in roadmaps
verification revision 1.2 
      1     $NetBSD: verification,v 1.2 2019/06/17 17:45:18 kamil Exp $
      2     
      3     NetBSD Verification Roadmap
      4     ===========================
      5     
      6     This roadmap covers things that we intend or would like to do pursuant
      7     to verification and quality control.
      8     
      9     The following elements, projects, and goals are relatively near-term:
     10     
     11      1. Cut down the Coverity backlog
     12      3. Deploy clang-static-analyzer
     13     
     14     The following elements, projects, and goals are longer-term:
     15     
     16      4. mint
     17      5. Database-driven program analyzer
     18     
     19     The following elements, projects, and goals are rather blue-sky so far:
     20     
     21      6. Use Frama-C to verify fsck_ffs
     22     
     23     
     24     Explanations
     25     ============
     26     
     27     1. Cut down the Coverity backlog
     28     
     29     Coverity provides us with free analysis reports, which we sometimes
     30     handle and sometimes don't. Apparently though Linux has a lower number
     31     of Coverity hits per line than we do; that seems fundamentally wrong
     32     and something that should get attention. Most of the problems Coverity
     33     finds are pretty easily fixed, or are false positives.
     34     
     35      - As of January 2017 coypu has been working on this. Christos often
     36        also fixes these.
     37      - There is currently no clear timeframe or release target.
     38      - Contact christos for further information.
     39     
     40     
     41     3. Deploy clang-static-analyzer
     42     
     43     There is some makefile support for running clang-static-analyzer, but
     44     it doesn't get done regularly. This should probably get added to the
     45     autobuilds.
     46     
     47      - As of January 2017 nobody is known to be working on this.
     48      - There is currently no clear timeframe or release target.
     49      - Contact joerg for further information.
     50     
     51     
     52     4. mint
     53     
     54     A while back dholland started on a replacement for the existing lint,
     55     since lint is not really smart enough to be useful and its code is
     56     only marginally maintainable. The code is in othersrc, but it needs
     57     some tidying before anyone else tries hacking on it.
     58     
     59      - As of January 2017 nobody is known to be working on this.
     60      - There is currently no clear timeframe or release target.
     61      - Responsible: dholland
     62     
     63     
     64     5. Database-driven program analyzer
     65     
     66     In the long run we would like to have a program analyzer that can
     67     scale to the whole kernel and can do differential analyses across
     68     different versions. This is a nontrivial project though.
     69     
     70      - As of January 2017 nobody is known to be working on this.
     71      - There is currently no clear timeframe or release target.
     72      - Contact: dholland
     73     
     74     
     75     6. Use Frama-C to verify fsck_ffs
     76     
     77     Frama-C is a framework for doing formal verification of C code using
     78     (mostly) precondition/postcondition specs. It is not everything one
     79     necessarily wants in a verification framework; but on the other hand
     80     it exists and people do use it.
     81     
     82     fsck_ffs seems like a good candidate for this because it's
     83     mission-critical and what it needs to do is comparatively well
     84     understood even in detail. However, the code may be too messy.
     85     
     86      - As of January 2017 nobody is known to be working on this.
     87      - There is currently no clear timeframe or release target.
     88      - Contact: dholland
     89