From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.org/gmane.linux.lib.musl.general/9886 Path: news.gmane.org!not-for-mail From: Joe Duarte Newsgroups: gmane.linux.lib.musl.general Subject: Formal verification of MUSL Date: Sun, 10 Apr 2016 19:18:23 -0700 Message-ID: Reply-To: musl@lists.openwall.com NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary=001a113ed540b5e48d05302c2870 X-Trace: ger.gmane.org 1460341134 11867 80.91.229.3 (11 Apr 2016 02:18:54 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 11 Apr 2016 02:18:54 +0000 (UTC) To: musl@lists.openwall.com Original-X-From: musl-return-9899-gllmg-musl=m.gmane.org@lists.openwall.com Mon Apr 11 04:18:51 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 1apRRC-0002PU-Qq for gllmg-musl@m.gmane.org; Mon, 11 Apr 2016 04:18:50 +0200 Original-Received: (qmail 3450 invoked by uid 550); 11 Apr 2016 02:18:48 -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 3371 invoked from network); 11 Apr 2016 02:18:35 -0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:date:message-id:subject:from:to; bh=XhiB1q6ui3/Q5rpGHKvAFWuv5FR3uzHjFUykxQj7mMo=; b=Jf4Aa2uySGfuLFndfC3gVXMNuy8acXFxvQjHJlMwkyZZqtaS5C2x02hJMmfjsV2+cc brusIoi4msUYOxG9EiV+IZYQHMkjeOHD6daf9efYVfUu83avCmmw+XlDsow4WU7MsTFs HXJ8mh/uVA2oTn9jJwZ8LSbWHRqqwnCon1qu+6sT95TcErpUYfzTRThOOEjO8+NTR7pX EqtPB2WWjrCapWEpGhr8Cxhtrv6mDGrHU1yv4N/36QvJY7AZQqz6FLcBHuI7mU+hCCVm ql1QUyFCUSMzMbm8z0p+2lzcqESrD0QpirjlC31k52glH2hvhYsVY0fywAFh65VjphhN 1XCw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:date:message-id:subject:from:to; bh=XhiB1q6ui3/Q5rpGHKvAFWuv5FR3uzHjFUykxQj7mMo=; b=UMotg7jWg+uqOdXNKTF+N+UfGnoIQ1b+/+5FlmbJbaNq9gLZhGygYGDRnS9c4f+H09 gQ9c6+L1OdUiDNHfsZloBQRL1mmjxwVdZWT+asSNeOLAUS/fksyp9YDLOO++3t/Y1n0L +iF5JvoSdA6Cf/LAhsKFl40UNwZHfLJrv6CCEm1fBY51Bm4tqDrAAuU052KjIBagZZ6X vX48082mGaawav65zse5ZkMOqAfYWSakDGPhL33gQWnfhAWP8s8JF0cs+S74TdoHX2Kg 08q4Mz1Grn3CmEmXVNWocl0m+ZUE9iQMWRZmrB+lqquc8m5MHWeFharoals7xvRqY96o k1pQ== X-Gm-Message-State: AD7BkJK66nwABbA3r1GRZRUVV+wXM1OyUYprNDaPh+VBQXWHqKBA9mmuTeIg4upaZlGlstIVdSTU2YguMFfGvg== X-Received: by 10.107.137.101 with SMTP id l98mr20501472iod.31.1460341103252; Sun, 10 Apr 2016 19:18:23 -0700 (PDT) Xref: news.gmane.org gmane.linux.lib.musl.general:9886 Archived-At: --001a113ed540b5e48d05302c2870 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hi all, Has there been any discussion of getting MUSL into a formally verified state? What would it take? 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. 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 =E2=80=93 is this feasible? In any case, whether an external audit or house project, I'm in for fifty bucks at least. Cheers, Joe Duarte 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. --001a113ed540b5e48d05302c2870 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hi all,

Has there been any discuss= ion of getting MUSL into a formally verified state? What would it take?

I'm a bit concerned about v= ulnerabilities like=C2=A0CVE-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-tri= vial C software or libraries are likely to have exploitable memory issues a= t any arbitrary time point / at all times including the present. This basel= ine reality strikes me as strange.

I started wondering about the possibilities for MUSL after seeing th= is write-up from the formally verified seL4 microkernel project:=C2=A0http://ssrg.nic= ta.com.au/projects/TS/l4.verified/proof.pml

I draw your attention = to the bottom section titled What the Proof Implies. It looks impres= sive. Their source code is here: https:= //github.com/seL4

The other piece for me was John Regehr's post on Tr= ustInSoft's audit of the PolarSSL library: http://blog.regehr.org/archives/1261

I think what th= ey 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 maintainabl= e and somewhat automated would be ideal. I've never messed with theorem= provers and formal verification =E2=80=93 is this feasible? In any case, w= hether an external audit or house project, I'm in for fifty bucks at le= ast.

Cheers,

Joe Duarte

p.s. I don't see MUSL on the free Coverity deal (https://scan.coverity.com/proje= cts). I think the LibreOffice devs got some good insights from it.
<= br>

--001a113ed540b5e48d05302c2870--