Steve Zdancewi
(University of Pennsylvania)is giving a talk on his work on
Verifying LLVM IR Code
hosted by Derek Dreyer( MPI-SWS talk in Kooperation mit dem Fachbereich Informatik)
LLVM is an industrial-strength compiler that's used for everything from day-to-day iOS development (in Swift) to pie-in-the-sky academic research projects. This makes the LLVM framework a sweet spot for bug-finding and verification technologies--any improvements to it are amplified across its many applications.
This talk asks the question: what does LLVM code _mean_, and, how can we ensure that LLVM-based tools (compilers, optimizers, code instrumentation passes, etc.) do what they're supposed to -- especially for safety- or security-critical applications? The Verified LLVM project (Vellvm) is our attempt to provide an answer. Vellvm gives a semantics to LLVM IR programs in the Coq interactive theorem prover, which can be used for developing machine-checkable formal properties about LLVM IR programs and transformation passes.
Our approach to modeling LLVM IR semantics uses _interaction trees_, a data structure that is suitable for representing impure, possibly nonterminating programs in dependent type theory. Interaction trees support compositional and modular reasoning about program semantics but are also executable, and hence useful for implementation and testing. We'll see how interaction trees are used in Vellvm and, along the way, we'll get a taste of what LLVM code looks like including some of its trickier semantic aspects. We'll also see (at a high level) how modern interactive theorem provers--in this case, Coq--can be used to verify compiler transformations.
No experience with LLVM or formal verification technologies will be assumed.
Bio: Dr. Zdancewic is a Full Professor and Associate Department Chair in Computer and Information Science at the University of Pennsylvania. He received his Ph.D. in Computer Science from Cornell University in 2002, and he graduated from Carnegie Mellon University with a B.S. in Computer Science and Mathematics in 1996. He is the recipient of an NSF Graduate Research Fellowship, an Intel fellowship, an NSF CAREER award, and a Sloan Fellowship. His numerous publications in the areas of programming languages and computer security include several best paper awards.
Dr. Zdancewic's research centers around using programming languages technology to help build secure and reliable software. He has worked on type-based enforcement of both information-flow and authorization policies, compiler techniques for ensuring memory safety of legacy C code, and, more recently, on using interactive theorem-proving technology to construct highly-trustworthy compiler optimization passes. His interests also include type theory and linear logics, and applications of those ideas.
| Time: | Wednesday, 13.01.2021, 15:00 |
|---|---|
| Place: | Join Zoom Meeting |
| Video: | https://zoom.us/j/99600775577?pwd=b21ZcTUyU2Z0N1VUUTRpa3JQWllyUT09 |
Termin als 
Datei downloaden und in den Kalender importieren.