CyLab

Distinguished Seminar: Usable Architecture-Based Security in the Wyvern Language with Jonathan Aldrich

October 22, 2018

11:30 a.m. - 12:30 p.m. ET

CIC, Panther Hollow Room

Jonathan Aldrich
Professor
School of Computer Science

This event is part of the CyLab Distinguished Seminar Series.

Abstract

A well-known, principled approach to software security is to build desired properties into the application architecture.  Unfortunately, this approach fails too often in practice, because we have inadequate support for writing down and enforcing the security architecture of a system.  The Wyvern programming language allows developers to express architectural design and system-level security properties within code, and provides usable mechanisms for enforcing both of these.  Based on results from type theory as well as user experiments, we'll describe how Wyvern's immutability types enforce the transitive integrity of data structures, how its type-specific languages can eliminate command injection attacks, and how a few lines of top-level code can enforce system-wide architectural properties.

Speaker Bio

Aldrich, JonathanJonathan 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 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.

Upcoming Events