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.

AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Saarbrücken

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.

--

Please contact office for the Zoom details.

Danielle Dalton

+49 681 9303 9106

--email hidden

passcode not visible

logged in users only

Join Zoom Meeting
https://zoom.us/j/99600775577?pwd=b21ZcTUyU2Z0N1VUUTRpa3JQWllyUT09

Meeting ID: 996 0077 5577
Passcode: 906631
One tap mobile
+496971049922,,99600775577# Germany
+493056795800,,99600775577# Germany

Dial by your location
        +49 69 7104 9922 Germany
        +49 30 5679 5800 Germany
        +49 69 3807 9883 Germany
        +49 695 050 2596 Germany
        +1 301 715 8592 US (Germantown)
        +1 312 626 6799 US (Chicago)
        +1 346 248 7799 US (Houston)
        +1 646 558 8656 US (New York)
        +1 669 900 9128 US (San Jose)
        +1 253 215 8782 US (Tacoma)
Meeting ID: 996 0077 5577
Find your local number: https://zoom.us/u/abQNBhDbku

Join by SIP
99600775577@zoomcrc.com

Join by H.323
162.255.37.11 (US West)
162.255.36.11 (US East)
115.114.131.7 (India Mumbai)
115.114.115.7 (India Hyderabad)
213.19.144.110 (Amsterdam Netherlands)
213.244.140.110 (Germany)
103.122.166.55 (Australia)
149.137.40.110 (Singapore)
64.211.144.160 (Brazil)
69.174.57.160 (Canada)
207.226.132.110 (Japan)
Meeting ID: 996 0077 5577
Passcode: 906631