From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.org/gmane.linux.lib.musl.general/9897 Path: news.gmane.org!not-for-mail From: Joe Duarte Newsgroups: gmane.linux.lib.musl.general Subject: Re: Formal verification of MUSL Date: Mon, 11 Apr 2016 18:00:24 -0700 Message-ID: References: <20160411042313.GT21636@brightrain.aerifal.cx> Reply-To: musl@lists.openwall.com NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary=001a1134dbeca866be05303f2fb2 X-Trace: ger.gmane.org 1460422843 11305 80.91.229.3 (12 Apr 2016 01:00:43 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Tue, 12 Apr 2016 01:00:43 +0000 (UTC) To: musl@lists.openwall.com Original-X-From: musl-return-9910-gllmg-musl=m.gmane.org@lists.openwall.com Tue Apr 12 03:00:39 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 1apmh5-0007Ug-5Q for gllmg-musl@m.gmane.org; Tue, 12 Apr 2016 03:00:39 +0200 Original-Received: (qmail 30220 invoked by uid 550); 12 Apr 2016 01:00:36 -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 30199 invoked from network); 12 Apr 2016 01:00:36 -0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to; bh=8PmGHco3MVpU90r+e5UKjM3dbJEU74vBIcBeIUN8v/0=; b=YyHl+Tvpq6T2fV4oRGMz4GyXXKZGH47myMqv9V/eRRpDjyX/QwCYMN8m9bvbL/wNAw PA44PnlOgUDPiIO+02PDLweZUdQIof/UR9jTe+pJPLGOkUXH5i1DCJGYV5d/RKN8StE/ ERKrXKO/P5i3dk1O4YCsECd2wGh9e7OaFIwHF9g4e8opGuEScwEb+YhdZz0lF90erYst MQ4iWTIr6xQFFgUD8BbEBf4Hb+uZRugOMgiuvBMqx+bfBMj7Zkiu9KiG3Z7vETpE9YrM 221OkA3lUbY5tdlSjb73PRCu7cCO+dwPAEwkNIuJD5jOmm/3LSyV+s+/fBRSxtQAN63o oNMw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:date :message-id:subject:from:to; bh=8PmGHco3MVpU90r+e5UKjM3dbJEU74vBIcBeIUN8v/0=; b=lr6WzvyzwbDAJ9uuo1b1FbOYqDggqJ6Kgw2GmESw0bDgr4zHM+ql+2uSv4AkN3ZGXu BUAs4C2+QzBRTFSic0nfVIoHaTRQfaO6oSSZ+j/H9xVFO/70za5MgVHhm/rzNZv2iLVJ gPEAk6GuGwkX051odUaymh8z8eE0jTG+O+F7h3GavEisni/8nfKqCKIAfL8PQpkwr9t9 QhB+vVqnryllFx/QSgORPBTe8YuLP79vRJF1TlW16MiK6t4bn8skbigT0SmCvK/8jO6V VAqT84rzekq2nb1PWW9zE3zk+BcYIj8YLR132u9sUJfRtzvSDOiw6VbgNtzUw68cefKU Oh3g== X-Gm-Message-State: AD7BkJLpgj/cbQn+8NVfvL4uJEXJLN8F1XTOEy2PTZLBVZ1imQNksJS8wGL8YAmi6Y4OelJXnqXSocJU/SjWcw== X-Received: by 10.50.155.67 with SMTP id vu3mr20563278igb.52.1460422824189; Mon, 11 Apr 2016 18:00:24 -0700 (PDT) In-Reply-To: Xref: news.gmane.org gmane.linux.lib.musl.general:9897 Archived-At: --001a1134dbeca866be05303f2fb2 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable > > > > > I have registered > > > > https://scan.coverity.com/projects/libc-musl > > "You are not authorized to access this page." > I have no experience with Coverity, but I guess you missed a step to make > it public. (The search also comes up empty.) > =E2=80=8BYes, I noticed that as well. It gave me the same "not authorized" = message. Normally, we should be able to add the project to our personal Coverity accounts by going to My Dashboard (top), click the Add a New Project button, then search for the project. Currently, musl is still not showing up in the search =E2=80=93 maybe it takes a couple of days to show? Nagy, everything you said sounds right. What about unikernels? Long-term, I'm more interested in running unikernels than in running Linux, BSD, or Windows. I'm thinking of something lik e OSv =E2=80=8B, where they built an ELF linker from scratch, as well as implemen= ting the Linux system calls: https://github.com/cloudius-systems/osv/wiki/Components-of-OSv In their case, they were going for glibc compatibility, and I assume a straight musl implementation would be easier. This ultimately gets at the separation of OS syscalls and ABIs vs. the libc. What if I have an OS or unikernel that doesn't know anything about C or POSIX, where C isn't a first-class citizen so much as an honored guest? musl-leveraging C applications would presumably be statically compiled in that case (and perhaps containerized), but there would also need be an ABI layer that is unclear to me. (Maybe this is relevant: How to Run POSIX Apps in a Minimal Picoprocess: http://research.microsoft.com/apps/pubs/default.aspx?id=3D1834= 61 -- which they might be drawing from in their recently announced bash or Ubuntu support. How they emulated the Linux ABI in that paper is very interesting.) I think the formal verification task would be simplified if we could shrink the ABI down in a unikernel or similar context, but I've only just begun to think about this. On floating point, the C ompCert team just published a new paper on verified compilation of floating point computations: =E2=80=8B =E2=80=8B https://hal.inria.fr/hal-00862689 =E2=80=8B =E2=80=8B It looks like nice work. Cheers, Joe --001a1134dbeca866be05303f2fb2 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

>
> I have registered
>
> https://scan.coverity.com/projects/libc-musl

"You are not authorized to access this page= ."
I have no experience with Coverity, but I guess you missed a step to make i= t public. (The search also comes up empty.)


=E2=80=8BYes, I noticed that as well. It gave me the same "not aut= horized" message. Normally, we should be able to add the project to ou= r personal Coverity accounts by going to My Dashboard (top), click the Add = a New Project button, then search for the project. Currently, musl is still= not showing up in the search =E2=80=93 maybe it takes a couple of days to = show?

=
Nagy, everything you said sounds right. What ab= out unikernels? Long-term, I'm more interested in running unikernels th= an in running Linux, BSD, or Windows. I'm thinking of something like OSv
=E2=80=8B, whe= re they built an ELF linker from scratch, as well as implementing the Linux= system calls: https://github.com/cloudius-systems/osv/wiki/Components-of-O= Sv

In their case, they were going for glibc compa= tibility, and I assume a straight musl implementation would be easier. This= ultimately gets at the separation of OS syscalls and ABIs vs. the libc. Wh= at if I have an OS or unikernel that doesn't know anything about C or P= OSIX, where C isn't a first-class citizen so much as an honored guest? = musl-leveraging C applications would presumably be statically compiled in t= hat case (and perhaps containerized), but there would also need be an ABI l= ayer that is unclear to me. (Maybe this is relevant: How to Run POSIX Apps = in a Minimal Picoprocess: http://research.microsoft.com/apps/pubs/default= .aspx?id=3D183461 -- which they might be drawing from in their recently= announced bash or Ubuntu support. How they emulated the Linux ABI in that = paper is very interesting.)
<= br>
I think the formal verifi= cation task would be simplified if we could shrink the ABI down in a uniker= nel or similar context, but I've only just begun to think about this.

On floating point, the C
ompCert team just= published a new paper on verified compilation of floating point computatio= ns:
=E2=80=8B =E2=80=8B
https://hal.inria.fr/hal-00862689
=E2=80=8B =C2=A0=E2=80=8BIt looks like nice work.

Cheers,

Joe


--001a1134dbeca866be05303f2fb2--