[llvm-dev] Question about Formal Verification

Mon Feb 29 19:05:04 PST 2016

Hmm, looks like I missed your email. This is a cool subject, so I'll try to catch up.

I have some memory of a company that did something similar (to LLBMC) with LLVM, but that may be cryptogenesis.

 > I am wondering whether anyone has tried using LLVM to apply formal verification to program code. 

Personally, I dream of the day when I can truly formally verify software with portable open source tools. Right now with LLVM & Clang we're really far from that day, but Clang's static analyzer can find plenty of bugs right now.

> conservatively, I suppose, since knowing the full behavior of arbitrary programs is probably reducible to the halting problem but to my knowledge one can always come up with a more constrained check for which failure merely leaves unknowns rather than trying to resolve halting-problem-equivalent questions.

I have a similar feeling we can *avoid* most halting-problem-esque issues through the careful use of annotations - basically the kind of "constrained check" you refer to - which allow programmers to specify intentions of their code. I've linked to it elsewhere (and can't look it up right now), but one of the major benefits of annotations is that they enable local analysis to detect issues that'd otherwise require global analysis (whole program dataflow, control flow, and friends), like overrunning dynamically sized buffers by passing the wrong integer to memcpy, or (more insidiously) doing something that's *technically* correct, but will break behavior.

I think Microsoft's SAL is the most developed annotation language, but it's proprietary, and poorly documented. The guys at OSR (they develop kernel mode code that needs to be correct, otherwise you bugcheck, or worse) REALLY like it, and you can see their enthusiasm for it on the NTDEV forum. I recall one post where they remarked about how astonishingly common it is for them to annotate mature and heavily tested (15 years+) code, and suddenly find all kinds of bugs (especially code that's "accidentally" correct). They mentioned that the aforementioned experience would instantly convert Linux-background programmers to SAL. For a few months after discovering it myself, I couldn't stand even the idea that I might ever again need to write code without SAL. I still find it annoying that I don't have portable versions of the _In_z_, _Out_z_, _Ret_z_, _Pre_z_, _Post_z_, and _Field_z_ , annotations, because null-terminated-ness isn't really assert()able. 

Ok, I'm digressing. Back to specifications.

There are two other things you should look into.

1. Frama-C  (Framework for Modular Analysis of C programs), frama-c.com
2. ACSL (ANSI/ISO C Specification Language), which Frama-C supports

They're both very cool. I'm not very familiar with Frama-C (entirely my own fault, haven't gotten around to it), but it does all kinds of correctness proofs, specified in ACSL. I'm also dissuaded by the fact that it's (seemingly) not integrated with compilation, which makes it yet another annoying hurdle preventing more widespread use.

> and I'm a software developer kicking around various wild ideas. (I wish I had something more interesting to say about myself than that, but nothing comes to mind; my day job is in SQL and Java, nothing to do with LLVM.)

You have nothing to be ashamed of! You're curious, and you're thinking about one of the larger issues underlying all the great struggles of software development. That seems pretty interesting to me. Always keep your curiosity alive :)

sent from my (stupid) windows phone

-----Original Message-----
From: "Scott Santucci via llvm-dev" <llvm-dev at lists.llvm.org>
Sent: ‎2/‎29/‎2016 7:19 PM
To: "llvm-dev at lists.llvm.org" <llvm-dev at lists.llvm.org>
Subject: Re: [llvm-dev] Question about Formal Verification

I'd just like to thank everyone who replied on this; the suggestions and resources are very helpful!

~Scott

On Tue, Feb 9, 2016 at 8:38 PM, Andrew Santosa <santosa_1999 at yahoo.com> wrote:

LLBMC http://llbmc.org uses bounded model checking technique to find errors in LLVM IR.
Model checking is essentially search, and since LLBMC is bounded, the search for errors is usually
incomplete, hence the approach may not verify the entire program, however, it may be good
enough to find interesting errors.

Best wishes,
Andrew

On Monday, 8 February 2016, 21:54, Scott Santucci via llvm-dev <llvm-dev at lists.llvm.org> wrote:

Hello, all,
My name is Scott Santucci and I'm a software developer kicking around various wild ideas. (I wish I had something more interesting to say about myself than that, but nothing comes to mind; my day job is in SQL and Java, nothing to do with LLVM.)
I am wondering whether anyone has tried using LLVM to apply formal verification to program code. I'm thinking about trying to develop tools that would leverage LLVM to check whether a program meets a design specification -- conservatively, I suppose, since knowing the full behavior of arbitrary programs is probably reducible to the halting problem but to my knowledge one can always come up with a more constrained check for which failure merely leaves unknowns rather than trying to resolve halting-problem-equivalent questions. Anyway, I figure I should start by finding out if there is prior work in that area. If this isn't the best place to ask, feel free to direct me elsewhere.
Thanks,
Scott

_______________________________________________
LLVM Developers mailing list
llvm-dev at lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20160229/8c9300a8/attachment.html>