From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.org/gmane.linux.lib.musl.general/9890 Path: news.gmane.org!not-for-mail From: Rich Felker Newsgroups: gmane.linux.lib.musl.general Subject: Re: Formal verification of MUSL Date: Mon, 11 Apr 2016 00:23:13 -0400 Message-ID: <20160411042313.GT21636@brightrain.aerifal.cx> References: Reply-To: musl@lists.openwall.com NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1460348609 15170 80.91.229.3 (11 Apr 2016 04:23:29 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 11 Apr 2016 04:23:29 +0000 (UTC) To: musl@lists.openwall.com Original-X-From: musl-return-9903-gllmg-musl=m.gmane.org@lists.openwall.com Mon Apr 11 06:23:28 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 1apTNo-0005z9-LX for gllmg-musl@m.gmane.org; Mon, 11 Apr 2016 06:23:28 +0200 Original-Received: (qmail 3848 invoked by uid 550); 11 Apr 2016 04:23:27 -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 3827 invoked from network); 11 Apr 2016 04:23:26 -0000 Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.21 (2010-09-15) Original-Sender: Rich Felker Xref: news.gmane.org gmane.linux.lib.musl.general:9890 Archived-At: 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. > I'm a bit concerned about vulnerabilities like CVE-2015-1817 from March of > last year. MUSL is a safer bet than the alternatives, but we still seem to > occupy a universe where all non-trivial C software or libraries are likely > to have exploitable memory issues at any arbitrary time point / at all > times including the present. This baseline reality strikes me as strange. Indeed. > I started wondering about the possibilities for MUSL after seeing this > write-up from the formally verified seL4 microkernel project: > http://ssrg.nicta.com.au/projects/TS/l4.verified/proof.pml > > I draw your attention to the bottom section titled *What the Proof Implies*.. > It looks impressive. Their source code is here: https://github.com/seL4 > > The other piece for me was John Regehr's post on TrustInSoft's audit of the > PolarSSL library: http://blog.regehr.org/archives/1261 > > I think what they did was a bit less formal and perhaps less laborious than > what the seL4 project team did, but it's still pretty neat, and probably > quite rare. Their report, or "verification kit", is here: > http://trust-in-soft.com/polarSSL_demo.pdf > > I assume that external audits aren't cheap. Something maintainable and > somewhat automated would be ideal. I've never messed with theorem provers > and formal verification – is this feasible? In any case, whether an > external audit or house project, I'm in for fifty bucks at least. One thing you have going for you with libc is that there's not a lot of interdependency; most components could be treated individually. Of course the big important ones like stdio have a lot of internal complexity themselves (and some "gratuitous UB" we need to fix due in stdio's case to the awful buffer pointer model we inherited). The worst part is probably proving correctness of thread synchronization primitives and related code. > p.s. I don't see MUSL on the free Coverity deal ( > https://scan.coverity.com/projects). I think the LibreOffice devs got some > good insights from it. What's needed to get it there? Rich