From owner-freebsd-current Thu Sep 10 11:30:43 1998 Return-Path: Received: (from majordom@localhost) by hub.freebsd.org (8.8.8/8.8.8) id LAA24674 for freebsd-current-outgoing; Thu, 10 Sep 1998 11:30:43 -0700 (PDT) (envelope-from owner-freebsd-current@FreeBSD.ORG) Received: from smtp03.primenet.com (smtp03.primenet.com [206.165.6.133]) by hub.freebsd.org (8.8.8/8.8.8) with ESMTP id LAA24645; Thu, 10 Sep 1998 11:30:28 -0700 (PDT) (envelope-from tlambert@usr08.primenet.com) Received: (from daemon@localhost) by smtp03.primenet.com (8.8.8/8.8.8) id LAA29902; Thu, 10 Sep 1998 11:30:18 -0700 (MST) Received: from usr08.primenet.com(206.165.6.208) via SMTP by smtp03.primenet.com, id smtpd029774; Thu Sep 10 11:30:07 1998 Received: (from tlambert@localhost) by usr08.primenet.com (8.8.5/8.8.5) id LAA27149; Thu, 10 Sep 1998 11:30:03 -0700 (MST) From: Terry Lambert Message-Id: <199809101830.LAA27149@usr08.primenet.com> Subject: Re: FreeBSD Hardening To: andrew@squiz.co.nz Date: Thu, 10 Sep 1998 18:30:03 +0000 (GMT) Cc: enkhyl@hayseed.net, security@FreeBSD.ORG, current@FreeBSD.ORG In-Reply-To: from "Andrew McNaughton" at Sep 10, 98 03:10:30 pm X-Mailer: ELM [version 2.4 PL25] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: owner-freebsd-current@FreeBSD.ORG Precedence: bulk X-Loop: FreeBSD.ORG > 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