From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.org/gmane.linux.lib.musl.general/9898 Path: news.gmane.org!not-for-mail From: Isaac Dunham Newsgroups: gmane.linux.lib.musl.general Subject: Re: Formal verification of MUSL Date: Mon, 11 Apr 2016 19:47:35 -0700 Message-ID: <20160412024734.GB20359@newbook> 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=utf-8 Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1460429286 5018 80.91.229.3 (12 Apr 2016 02:48:06 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Tue, 12 Apr 2016 02:48:06 +0000 (UTC) To: musl@lists.openwall.com Original-X-From: musl-return-9911-gllmg-musl=m.gmane.org@lists.openwall.com Tue Apr 12 04:47:54 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 1apoMr-0006vC-DU for gllmg-musl@m.gmane.org; Tue, 12 Apr 2016 04:47:53 +0200 Original-Received: (qmail 19884 invoked by uid 550); 12 Apr 2016 02:47:51 -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 19866 invoked from network); 12 Apr 2016 02:47:50 -0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=date:from:to:subject:message-id:references:mime-version :content-disposition:content-transfer-encoding:in-reply-to :user-agent; bh=6aRNPRZhEi5f/lDmtxRW1U4GxT4N5Jv/yEhD5s/1apA=; b=VduJATeuCvwmqa6FTplZETeCK+UfsCIWHWeIRQZgs2VfKDlDZiP0t0vhjnX2PvzJYR TTMILtUsKWvDG6/dWJRx0xC1W4GW6LTIzxDRHvelNb4CHPnbpvE8U/mAR/qcuM7y3+1g 3ghtMSa0VC5MhXe0mHdr0zPVuI3eXqEEvVGq6442OCkTuzYGlSb1z9CDt/3afqr4FWG9 HBA8HjcVceHE/DlP0v6GLHFGm5HyvE5Q67AfutTKxQjeLo9KFCXPmTV6XmFlkhUHBukz XOdOGGpuz5WtIE5Lz/OKd06oaPIU4Zi0lsiQwxQBkGOapu4DHpNi/+SktAVQU5vcXUAW dOxQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:date:from:to:subject:message-id:references :mime-version:content-disposition:content-transfer-encoding :in-reply-to:user-agent; bh=6aRNPRZhEi5f/lDmtxRW1U4GxT4N5Jv/yEhD5s/1apA=; b=XF6kFzO2gsV1uCrHWhcwskZvCmDM1rXsDx4hmDZRbDf8SYlgB8Hlvuge0wNFJ7NmCN 0q3dAyXYwqsAjODr22gaBYiJ4RpTQejGxzjn6h3me8mElcoayakKrsnhym/mZtpnpH9u tqTqI01uw9KY7pbBZ25JojgRMZaKIG1QCNzCdiHMIaOpcIZ2usqHVUBvLlaH+CCn6zrF hQnIfFyuvPF8jg7p4hb3UuswZJEPT2FT7fbq4oS60iqgIA6cX4VDSoaK9z5REyohW5vb VEMSjtHMkSUZ00sLpysm4dCgiYxB9q5T/0+q3MtsBgkiqxB9/zP/RHfd4c1O/az8rVQt GH1A== X-Gm-Message-State: AOPr4FWlOl6H7meuBitU4IXejquOMQreN4MmPimDBFcNB+OH551mvdj6zPZGy83l1KgeSg== X-Received: by 10.98.87.216 with SMTP id i85mr1173021pfj.61.1460429258532; Mon, 11 Apr 2016 19:47:38 -0700 (PDT) Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.6.0 (2016-04-01) Xref: news.gmane.org gmane.linux.lib.musl.general:9898 Archived-At: On Mon, Apr 11, 2016 at 06:00:24PM -0700, Joe Duarte wrote: > > > > > > > > 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.) > > > > ​Yes, 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 – 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 like OSv, where they built an ELF > linker from scratch, as well as implementing the Linux system calls: > https://github.com/cloudius-systems/osv/wiki/Components-of-OSv OSv uses a (rather old) version of musl, with some changes needed. If I understand correctly, they essentially changed musl so that rather than using syscalls, it would directly call the underlying kernel function. Another unikernel-type project using musl is the ELLCC "Embedded Little Kernel": http://ellcc.org/blog/?tag=elk And while we're discussing alternate hosts, I might as well mention that seL4 uses musl for the POSIX libc. > 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=183461 > -- 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: > ​ ​ > https://hal.inria.fr/hal-00862689 > ​ ​ > It looks like nice work. > > Cheers, > >