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