From owner-freebsd-security@FreeBSD.ORG Fri Apr 25 17:59:22 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 E22B6717; Fri, 25 Apr 2014 17:59:21 +0000 (UTC) Received: from st11p09mm-asmtp001.mac.com (st11p09mm-asmtp001.mac.com [17.164.24.96]) by mx1.freebsd.org (Postfix) with ESMTP id ABB791303; Fri, 25 Apr 2014 17:59:21 +0000 (UTC) MIME-version: 1.0 Content-type: text/plain; charset=windows-1252 Received: from discipline.rdnzl.info (dsl-hkibrasgw1-58c380-33.dhcp.inet.fi [88.195.128.33]) by st11p09mm-asmtp001.mac.com (Oracle Communications Messaging Server 7u4-27.08(7.0.4.27.7) 64bit (built Aug 22 2013)) with ESMTPSA id <0N4L00LF5LYN2G70@st11p09mm-asmtp001.mac.com>; Fri, 25 Apr 2014 17:59:15 +0000 (GMT) Subject: Re: OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + hole? From: Kimmo Paasiala In-reply-to: Date: Fri, 25 Apr 2014 20:59:09 +0300 Content-transfer-encoding: quoted-printable Message-id: <1705A4DB-6413-442E-8850-E629EC1702F2@icloud.com> References: <8783.1398202137@server1.tristatelogic.com> <20140423003400.GA8271@glaze.hydra> <20140423010054.2891E143D098@rock.dv.isc.org> <20140423012206.GB8271@glaze.hydra> <86bnvpoav7.fsf@nine.des.no> To: Ben Laurie X-Mailer: Apple Mail (2.1874) X-MANTSH: 1TEIXWV4bG1oaGkdHB0lGUkdDRl5PWBoaEhEKTEMXGx0EGx0YBBIZBBsSEBseGh8 aEQpYTRdLEQptfhcaEQpMWRcbGhsbEQpZSRcRClleF2hjeREKQ04XSxsbGmJCH2lmHlxCGXhzB xl6Gx0fE29+EQpYXBcZBBoEHQdNSx0SSEkcTAUbHQQbHRgEEhkEGxIQGx4aHxsRCl5ZF2FBb0l kEQpMRhdsa2sRCkNaFxISBBsTHwQbGBIEGRkRCkJeFxsRCkRYFx4RCkRJFx4RCkJFF2Z9fxNNb 1xgZRoSEQpCThdrRRpSUB5DXFlcaBEKQkwXbk0deVljZGh+GEYRCkJsF2FAfFNsSx8YZHt+EQp CQBdtZGRPRhIYZlwYTxEKcGcXbFAcemgbG2hDZmQRCnBoF2Jse29/GVBlR2cdEQpwaBdjbl8fU GdhY3wTQxEKcGgXbVlmHUBwWmcaTh4RCnBoF29OQ0ZOZkFyZ3NiEQpwaBdtBQVjWF1QGWl4SxE KcH8Xbm5oGhMdQ2AfXW0RCnBfF3pgHElhGxlcYF1lEQpwbBdtZ24FH2FOYRxbGxEKcEwXYVlhY UZwSVJbfWwR X-CLX-Spam: false X-CLX-Score: 1011 X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:5.11.96,1.0.14,0.0.0000 definitions=2014-04-25_05:2014-04-25,2014-04-25,1970-01-01 signatures=0 X-Proofpoint-Spam-Details: rule=notspam policy=default score=0 spamscore=0 suspectscore=35 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=7.0.1-1402240000 definitions=main-1404250277 Cc: =?windows-1252?Q?Dag-Erling_Sm=F8rgrav?= , "Ronald F. Guilmette" , "freebsd-security@freebsd.org security" 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: Fri, 25 Apr 2014 17:59:22 -0000 On 25.4.2014, at 17.15, Ben Laurie wrote: > On 25 April 2014 13:24, Dag-Erling Sm=F8rgrav wrote: >> Chad Perrin writes: >>> Obviously, human judgment is an important part of the process of = finding >>> and fixing bugs. If it wasn't, the last program we'd ever have to = debug >>> would be the one that finds and fixes bugs. >>=20 >> https://en.wikipedia.org/wiki/Halting_problem >>=20 >> Oh, wait, is this one of those conversations where knowledge and = facts >> are not welcome? >=20 > Curious what the halting problem can tell us about finding/fixing = bugs? >=20 It and its direct implications mean that it=92s provably impossible to = write a program X that would take another program A as its input and be = able to decide with 100% certainty whether this other program A has a = certain property or not. In the actual halting problem the property is =93The program runs to = completion and produces a result with every possible input=94. A classic = real world example is when property is set to =93The program A is/has a = virus=94. The halting problem applies to this discussion very naturally = if you use the property =93The program A has a buffer overflow = vulnerability=94 or =93The program A uses memory that has already been = free()=92d=94. None of these properties (or any other similar property) = can be detected programmatically with 100% certainty, that is what the = halting problem tells you about finding bugs. In essence all this is saying that is foolish to claim that an automated = code analyzer could find all bugs in a given piece of code, outside some = very trivial programs it is just not going to happen. =20 -Kimmo