From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.org/gmane.linux.lib.musl.general/9893 Path: news.gmane.org!not-for-mail From: Szabolcs Nagy Newsgroups: gmane.linux.lib.musl.general Subject: Re: Formal verification of MUSL Date: Mon, 11 Apr 2016 14:21:07 +0200 Message-ID: <20160411122107.GA22574@port70.net> References: <20160411042313.GT21636@brightrain.aerifal.cx> Reply-To: musl@lists.openwall.com NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1460377288 3847 80.91.229.3 (11 Apr 2016 12:21:28 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 11 Apr 2016 12:21:28 +0000 (UTC) To: musl@lists.openwall.com Original-X-From: musl-return-9906-gllmg-musl=m.gmane.org@lists.openwall.com Mon Apr 11 14:21:27 2016 Return-path: Envelope-to: gllmg-musl@m.gmane.org Original-Received: from mother.openwall.net ([195.42.179.200]) by plane.gmane.org with smtp (Exim 4.69) (envelope-from ) id 1apaqK-0003Kt-69 for gllmg-musl@m.gmane.org; Mon, 11 Apr 2016 14:21:24 +0200 Original-Received: (qmail 21548 invoked by uid 550); 11 Apr 2016 12:21:20 -0000 Mailing-List: contact musl-help@lists.openwall.com; run by ezmlm Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-ID: Original-Received: (qmail 21530 invoked from network); 11 Apr 2016 12:21:19 -0000 Mail-Followup-To: musl@lists.openwall.com Content-Disposition: inline In-Reply-To: <20160411042313.GT21636@brightrain.aerifal.cx> User-Agent: Mutt/1.5.24 (2015-08-30) Xref: news.gmane.org gmane.linux.lib.musl.general:9893 Archived-At: * Rich Felker [2016-04-11 00:23:13 -0400]: > On Sun, Apr 10, 2016 at 07:18:23PM -0700, Joe Duarte wrote: > > Has there been any discussion of getting MUSL into a formally verified > > state? What would it take? > > There's been some discussion (off-list) of using tis-interpreter on > musl, but that's not the same as formal verification. So far I'm not > aware of anything in the way of actual verification. > in general libc won't be formally verified until its api and the underlying platform are formally defined (i.e. the implemented posix api and underlying linux and toolchain behaviour) this won't happen any time soon. formal verification requires a precise model of the interface (which means an alternative implementation) and some annotation to help proving that the libc matches the model. this is a lot of work even for simple apis, it is more realistic to only prove some easy but practically useful property for a subset of the libc code, so you have to be more precise what you ask for. some properties are easy to model, but still hard to verify (e.g. ieee 754 arithmetics has formal models, but verifying the accuracy of math functions is hard.) some properties are easy to verify with moderate modelling effort (e.g. checking for posix namespace violations in libc headers). some properties are hard to verify, but easy to check at runtime with moderate overhead (e.g. signed int overflow checks with ubsan instrumentation). etc. checking for security issues is a small subset of formal verification (in c the most relevant property is probably well-defiend memory accesses).