1*975aab07Skamil$NetBSD: verification,v 1.2 2019/06/17 17:45:18 kamil Exp $ 2298a4bfaSdholland 3298a4bfaSdhollandNetBSD Verification Roadmap 4298a4bfaSdholland=========================== 5298a4bfaSdholland 6298a4bfaSdhollandThis roadmap covers things that we intend or would like to do pursuant 7298a4bfaSdhollandto verification and quality control. 8298a4bfaSdholland 9298a4bfaSdhollandThe following elements, projects, and goals are relatively near-term: 10298a4bfaSdholland 11298a4bfaSdholland 1. Cut down the Coverity backlog 12298a4bfaSdholland 3. Deploy clang-static-analyzer 13298a4bfaSdholland 14298a4bfaSdhollandThe following elements, projects, and goals are longer-term: 15298a4bfaSdholland 16298a4bfaSdholland 4. mint 17298a4bfaSdholland 5. Database-driven program analyzer 18298a4bfaSdholland 19298a4bfaSdhollandThe following elements, projects, and goals are rather blue-sky so far: 20298a4bfaSdholland 21298a4bfaSdholland 6. Use Frama-C to verify fsck_ffs 22298a4bfaSdholland 23298a4bfaSdholland 24298a4bfaSdhollandExplanations 25298a4bfaSdholland============ 26298a4bfaSdholland 27298a4bfaSdholland1. Cut down the Coverity backlog 28298a4bfaSdholland 29298a4bfaSdhollandCoverity provides us with free analysis reports, which we sometimes 30298a4bfaSdhollandhandle and sometimes don't. Apparently though Linux has a lower number 31298a4bfaSdhollandof Coverity hits per line than we do; that seems fundamentally wrong 32298a4bfaSdhollandand something that should get attention. Most of the problems Coverity 33298a4bfaSdhollandfinds are pretty easily fixed, or are false positives. 34298a4bfaSdholland 35298a4bfaSdholland - As of January 2017 coypu has been working on this. Christos often 36298a4bfaSdholland also fixes these. 37298a4bfaSdholland - There is currently no clear timeframe or release target. 38298a4bfaSdholland - Contact christos for further information. 39298a4bfaSdholland 40298a4bfaSdholland 41298a4bfaSdholland3. Deploy clang-static-analyzer 42298a4bfaSdholland 43298a4bfaSdhollandThere is some makefile support for running clang-static-analyzer, but 44298a4bfaSdhollandit doesn't get done regularly. This should probably get added to the 45298a4bfaSdhollandautobuilds. 46298a4bfaSdholland 47298a4bfaSdholland - As of January 2017 nobody is known to be working on this. 48298a4bfaSdholland - There is currently no clear timeframe or release target. 49298a4bfaSdholland - Contact joerg for further information. 50298a4bfaSdholland 51298a4bfaSdholland 52298a4bfaSdholland4. mint 53298a4bfaSdholland 54298a4bfaSdhollandA while back dholland started on a replacement for the existing lint, 55298a4bfaSdhollandsince lint is not really smart enough to be useful and its code is 56298a4bfaSdhollandonly marginally maintainable. The code is in othersrc, but it needs 57298a4bfaSdhollandsome tidying before anyone else tries hacking on it. 58298a4bfaSdholland 59298a4bfaSdholland - As of January 2017 nobody is known to be working on this. 60298a4bfaSdholland - There is currently no clear timeframe or release target. 61298a4bfaSdholland - Responsible: dholland 62298a4bfaSdholland 63298a4bfaSdholland 64298a4bfaSdholland5. Database-driven program analyzer 65298a4bfaSdholland 66298a4bfaSdhollandIn the long run we would like to have a program analyzer that can 67298a4bfaSdhollandscale to the whole kernel and can do differential analyses across 68298a4bfaSdhollanddifferent versions. This is a nontrivial project though. 69298a4bfaSdholland 70298a4bfaSdholland - As of January 2017 nobody is known to be working on this. 71298a4bfaSdholland - There is currently no clear timeframe or release target. 72298a4bfaSdholland - Contact: dholland 73298a4bfaSdholland 74298a4bfaSdholland 75298a4bfaSdholland6. Use Frama-C to verify fsck_ffs 76298a4bfaSdholland 77298a4bfaSdhollandFrama-C is a framework for doing formal verification of C code using 78298a4bfaSdholland(mostly) precondition/postcondition specs. It is not everything one 79298a4bfaSdhollandnecessarily wants in a verification framework; but on the other hand 80298a4bfaSdhollandit exists and people do use it. 81298a4bfaSdholland 82298a4bfaSdhollandfsck_ffs seems like a good candidate for this because it's 83298a4bfaSdhollandmission-critical and what it needs to do is comparatively well 84298a4bfaSdhollandunderstood even in detail. However, the code may be too messy. 85298a4bfaSdholland 86298a4bfaSdholland - As of January 2017 nobody is known to be working on this. 87298a4bfaSdholland - There is currently no clear timeframe or release target. 88298a4bfaSdholland - Contact: dholland 89