1$NetBSD: verification,v 1.2 2019/06/17 17:45:18 kamil Exp $
2
3NetBSD Verification Roadmap
4===========================
5
6This roadmap covers things that we intend or would like to do pursuant
7to verification and quality control.
8
9The following elements, projects, and goals are relatively near-term:
10
11 1. Cut down the Coverity backlog
12 3. Deploy clang-static-analyzer
13
14The following elements, projects, and goals are longer-term:
15
16 4. mint
17 5. Database-driven program analyzer
18
19The following elements, projects, and goals are rather blue-sky so far:
20
21 6. Use Frama-C to verify fsck_ffs
22
23
24Explanations
25============
26
271. Cut down the Coverity backlog
28
29Coverity provides us with free analysis reports, which we sometimes
30handle and sometimes don't. Apparently though Linux has a lower number
31of Coverity hits per line than we do; that seems fundamentally wrong
32and something that should get attention. Most of the problems Coverity
33finds 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
413. Deploy clang-static-analyzer
42
43There is some makefile support for running clang-static-analyzer, but
44it doesn't get done regularly. This should probably get added to the
45autobuilds.
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
524. mint
53
54A while back dholland started on a replacement for the existing lint,
55since lint is not really smart enough to be useful and its code is
56only marginally maintainable. The code is in othersrc, but it needs
57some 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
645. Database-driven program analyzer
65
66In the long run we would like to have a program analyzer that can
67scale to the whole kernel and can do differential analyses across
68different 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
756. Use Frama-C to verify fsck_ffs
76
77Frama-C is a framework for doing formal verification of C code using
78(mostly) precondition/postcondition specs. It is not everything one
79necessarily wants in a verification framework; but on the other hand
80it exists and people do use it.
81
82fsck_ffs seems like a good candidate for this because it's
83mission-critical and what it needs to do is comparatively well
84understood 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