Date: Thu, 10 Sep 1998 18:30:03 +0000 (GMT) From: Terry Lambert <tlambert@primenet.com> To: andrew@squiz.co.nz Cc: enkhyl@hayseed.net, security@FreeBSD.ORG, current@FreeBSD.ORG Subject: Re: FreeBSD Hardening Message-ID: <199809101830.LAA27149@usr08.primenet.com> In-Reply-To: <Pine.BSF.3.96.980910150215.328N-100000@aniwa.sky> from "Andrew McNaughton" at Sep 10, 98 03:10:30 pm
next in thread | previous in thread | raw e-mail | index | archive | help
> To get to a point where you can declare a piece of code correct is a > difficult thing to do, and is prone to getting it wrong. To find > something that needs fixing generally isn't all that difficult. Actually, if your code is in vanilla K&R C, or can be preprocessed into it (using the __P() macro and friends), then there is a tool in the comp.sources.c++ archives that can perform full branch-path analysis. This allows you to automatically generate code-coverage tests, which in turn allows you to build specification/validation tests by covering the boundary conditions noted in the branch paths. Taken together, this is most of the way to a "correctness proof". Now if instead of writing your unit tests in C (or some other languages, you instead write a data interface specification using the TET or ETET tool sets that are publically available (and were distributed by UNIX International), and which have, themselves, been tested for correctness with tools like "BattleMap", then you can come very close to closure on the idea of correctness. To handle the final boundary cases, you need to independently generate test data from two sources, tsort it, and compare the two for discrepancies. This is not impossible, but it is a lot of work. Most probably, you could get 95% of the way there merely by hand-coding the unit tests after the analysis, which is 95% better than where things stand today. See the comp.sources archives on gatekeeper.dec.com for the source code for the tool. Terry Lambert terry@lambert.org --- Any opinions in this posting are my own and not those of my present or previous employers. To Unsubscribe: send mail to majordomo@FreeBSD.org with "unsubscribe freebsd-current" in the body of the message
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?199809101830.LAA27149>