From owner-freebsd-security@FreeBSD.ORG Mon Apr 21 21:36:20 2014 Return-Path: Delivered-To: freebsd-security@freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [8.8.178.115]) (using TLSv1 with cipher ADH-AES256-SHA (256/256 bits)) (No client certificate requested) by hub.freebsd.org (Postfix) with ESMTPS id 2899DBAC for ; Mon, 21 Apr 2014 21:36:20 +0000 (UTC) Received: from gate2.quietfountain.com (gate2.quietfountain.com [97.64.213.195]) by mx1.freebsd.org (Postfix) with ESMTP id 01CE519DA for ; Mon, 21 Apr 2014 21:36:19 +0000 (UTC) Received: from ops1.quietfountain.com (ops1.quietfountain.com [192.168.29.13]) by gate2.quietfountain.com (Postfix) with ESMTP id 2E3C8B826A for ; Mon, 21 Apr 2014 16:36:13 -0500 (CDT) To: freebsd-security@freebsd.org Date: Mon, 21 Apr 2014 16:35:26 -0500 Subject: Re: De Raadt + FBSD + OpenSSH + hole? References: <53546795.9050304@quietfountain.com> <97711.1398112757@server1.tristatelogic.com> Message-ID: <53558F1E.1010308@quietfountain.com> From: "hcoin" Received: from [192.168.29.127] (gate1.quietfountain.com [192.168.29.2]) by ops1.quietfountain.com; Mon, 21 Apr 2014 16:35:38 -0500 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.4.0 MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-BeenThere: freebsd-security@freebsd.org X-Mailman-Version: 2.1.17 Precedence: list List-Id: "Security issues \[members-only posting\]" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 21 Apr 2014 21:36:20 -0000 On 04/21/2014 03:39 PM, Ronald F. Guilmette wrote: > > In message <53546795.9050304@quietfountain.com>, > "hcoin" wrote: > >> ... It is for the community to decide whether it is 'worth it' >> on a case by case basis given there is no way to prove a program >> 'correct' from a security perspective. > I guess that I was sick that day in software school. > > Did I just hear you tell me that I can't prove the following program > is "secure"? > > > int > main (void) > { > return 0; > } > _______________________________________________ > Good one. There were efforts, some years ago, to prove 'software correctness' with a similar understanding of 'correct' as mathematicians have when regarding a theorem as 'true'. The alligators in the complexity swamp ate those efforts before breakfast. First you have to prove the microcode in the processors correct, then you have to prove the compilers 'correctly' translate your favorite language into machine code, then you have to prove the OS is both 'correct' and doesn't 'break' the correctness in the running application. To manage that you have to extend logical expression to manage asynchronous events, no small thing. Our logical tools are pretty bound to linear 'if then' bricks-upon-other-bricks concepts. And then, after all that is proven, the question of whether the program you wrote is 'correct' can be engaged. The new-ish language Haskell takes an 'outside the box' approach to the question, by shifting what a 'program' is to be closer to 'what should the result be' than 'what step should happen next'. There's more hope such a language could specify provably correct programs than C-ish or object-oriented cousins, but that still leaves the whole machine-language domain unaddressed. Imagine the size of a number made up of every settable option bit in the processor and support chips, and add more for each occasion the order in which those bits are set or reset matters. Each combination of those bits calls for the correctness proof to be rechecked. Even in that little program you wrote, is it a security hole if, left on the stack upon return, the perhaps unused arguments remain? Just because you're paranoid doesn't mean they really aren't after you.