USI - Email

Archive / INF Seminars / INF_2019_06_25_Jonathan_Aldrich

USI - Email

	Obsidian: A Safe, Usable Language for Smart Contracts

Host: Prof. Matthias Hauswirth

Tuesday

25.06

USI Lugano Campus, room SI-003, Informatics building

14:30-15:30


	Jonathan Aldrich Carnegie Mellon University, USA

Abstract:
Smart contracts running on blockchain platforms automate contracts between participants who have not established mutual trust. Unfortunately, many smart contracts have had flaws resulting in millions of dollars in losses. Obsidian is a novel programming language with a type system that enables static detection of bugs that are common in smart contracts today. It uses typestate to detect improper state manipulation and uses linear types to detect abuse of assets. I will describe how we combined ideas from type theory with behavioral research methods in order to design a language that is safe while identifying and addressing usability issues with previous typestate approaches. I will also describe Obsidian's implementation and case studies we have performed in the areas of parametric insurance and supply chain management, showing that the language can express interesting smart contracts.

Biography:
Jonathan Aldrich is a Professor of Computer Science at Carnegie Mellon University. He is the director of CMU's Software Engineering Ph.D. program, and teaches courses in programming languages, software engineering, and program analysis for quality and security. Dr. Aldrich joined the CMU faculty after completing a Ph.D. at the University of Washington and a B.S. at Caltech.
Dr. Aldrich’s research centers around new languages for expressing software and its properties that improve our ability to engineer software securely at scale. His research contributions include verifying the correct implementation of an architectural design, modular formal reasoning about code, and API protocol specification and verification. For his work on software architecture, Aldrich received a 2006 NSF CAREER award and the 2007 Dahl-Nygaard Junior Prize, given annually for a significant technical contribution to object-oriented programming. He is currently working on the design of Wyvern, a programming language design for security and productivity; the development of a new Gradual Verification paradigm enabling incremental progress toward verified code; and novel domain-specific languages for visualizing mathematics and for smart contract/blockchain programming.