4 ms·

Unfortunately, I couldn't decipher the significance of this from the first paragraph. What does this mean for LLVM? How does it make working with LLVM better?

nickpsecurity 11y ago
It's part of verification work in general. One must have a formal way of representing a program before proving key properties (eg safety, security) about it. Formal verification also often uses refinement to move from abstract to concrete with intermediate forms in between. See CompCert compiler's stages for how that might apply to LLVM (front ends especially). Also, static analysis tools like Astree Analyzer or SPARK Ada's Examiner have some internal model of the language to analyze to prove absence of bugs. Formal semantics helps with them, too. So, it's kind of a foundation to build other work on that will let one rigorously verify the correct use, optimization, or compilation of LLVM programs. The link below has lots of examples of awesome work in security or verification that builds on LLVM. Some use Vellvm already with most able to benefit somehow if work is put in. http://llvm.org/pubs/ http://llvm.org/pubs/
geofft 11y ago
It uses Coq, a language for proving things about code (and writing code in a way you can prove things about), to interpret LLVM IR and verify the correctness of transformations on LLVM IR. IR ("intermediate representation") is the form of code inside the compiler, used after a frontend (like clang or rustc) has parsed and made sense of the particular language you're using, and before the compiler is ready to output native code. All optimizations happen on IR. So, this is a toolkit for letting you prove the correctness of LLVM optimizations (i.e., that some IR has the same behavior before and after the optimization pass), so that an optimization pass isn't accidentally introducing exploitable bugs into your software.

nickpsecurity 11y ago

It's part of verification work in general. One must have a formal way of representing a program before proving key properties (eg safety, security) about it. Formal verification also often uses refinement to move from abstract to concrete with intermediate forms in between. See CompCert compiler's stages for how that might apply to LLVM (front ends especially). Also, static analysis tools like Astree Analyzer or SPARK Ada's Examiner have some internal model of the language to analyze to prove absence of bugs. Formal semantics helps with them, too. So, it's kind of a foundation to build other work on that will let one rigorously verify the correct use, optimization, or compilation of LLVM programs. The link below has lots of examples of awesome work in security or verification that builds on LLVM. Some use Vellvm already with most able to benefit somehow if work is put in. http://llvm.org/pubs/ http://llvm.org/pubs/

geofft 11y ago

It uses Coq, a language for proving things about code (and writing code in a way you can prove things about), to interpret LLVM IR and verify the correctness of transformations on LLVM IR. IR ("intermediate representation") is the form of code inside the compiler, used after a frontend (like clang or rustc) has parsed and made sense of the particular language you're using, and before the compiler is ready to output native code. All optimizations happen on IR. So, this is a toolkit for letting you prove the correctness of LLVM optimizations (i.e., that some IR has the same behavior before and after the optimization pass), so that an optimization pass isn't accidentally introducing exploitable bugs into your software.