POP

Information-flow security-typed programming languages use types to statically enforce noninterference between potentially conspiring values, such as the arguments and results of functions.  But to adopt static security types, like other advanced type disciplines, programmers must adopt the discipline wholesale.

To provide a gentler path to security typing, researchers have designed languages that blend static and dynamic checking of security types.  Unfortunately most of these languages support static, type-based reasoning about noninterference if programs are entirely statically secured.  This limitation substantially weakens the benefits that dynamic enforcement brings to static security typing.

This talk describes GSLref, a security-typed higher-order language that supports gradual migration between a simple type discipline and security type discipline, using the principles underlying gradual typing.

GSLref satisfies most of the criteria set forth by Siek et al. for gradually-typed languages.  The one exception, called the "dynamic gradual guarantee" cannot be satisfied without violating noninterference.

To realize this design, we were led to draw a sharp distinction between syntactic type safety and semantic type soundness, each of which constrains the design of the gradual language.

Ronald Garcia is an associate professor of Computer Science at the University of British Columbia.  His research investigates how fundamental concepts in the theory, implementation, and practice of programming languages can improve the software development process.  His research has focused on static and dynamic type-based reasoning, metaprogramming, and generic programming.

Prior to his appointment at UBC, he was a Computing Innovation Fellow at Carnegie Mellon University and Postdoctoral Fellow at Rice University.   He received a PhD in Computer Science from Indiana University, and an MSc and BSc in Electrical Engineering from the University of Notre Dame.

The simply-typed λ-calculus, with only function types, is strongly normalizing, and its program equivalence relation is decidable: unlike in more advanced type system with polymorphism or effects, the natural "syntactic" equivalence (βη-equivalence) corresponds to natural "semantic" equivalence (observational or contextual equivalence), and is decidable. Adding product types (pairs) is easy and preserves these properties, but sums (disjoint unions) are, surprisingly, harder. It is only in 1995 that Neil Ghani proved that the equivalence in presence of sums is decidable, and the situation in presence of the empty type (zero-ary sum) was unknown.

 

We propose an equivalence algorithm for sums and the empty type that takes inspiration from a proof-theoretic technique, named "focusing", designed for proof search. The exposition will be introductory; I will present the difficulties caused by sums and the empty type, present some of the existing approaches for sums in the literature, introduce focusing, and give a high-level intuition of our saturation-based algorithm and its termination argument. No previous knowledge of focusing is assumed. I expect some familiarity with typed lambda-calculi, but will recall all concepts used (for example, βη-equivalence) during the talk.

Gabriel Scherer ("gasche") is a post-doctoral researcher at Northeastern University, Boston, working with Amal Ahmed on formal aspects multi-language programming systems.

 

Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs.  Relational program verification can be used for reasoning about a broad range of properties: information flow security, relative cost, sensitivity or continuity, differential privacy, etc. In a higher-order setting, relational program verification can be achieved using relational refinement type systems, a form of refinement types where assertions have a relational interpretation. Relational refinement type systems excel at relating structurally equivalent terms but provide limited support for relating terms with very different structures.

In this talk, he will present a logic, called Relational Higher Order Logic (RHOL), for proving relational properties of a simply typed λ-calculus with inductive types and recursive definitions.  RHOL retains the type-directed flavor of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms.  He will present some of the property of RHOL, some examples and sound embeddings for several existing relational type systems.  He will then briefly discuss two extensions of the basic RHOL for guarded recursion and for probabilistic programs.

Joint work with Alejandro Aguille, Gilles Barthe, Deepak Garg, and Pierre-Yves Strub

Marco Gaboardi is an assistant professor at the University at Buffalo, SUNY. Previously, he was a faculty at the University of Dundee, Scotland. He received his PhD from the University of Torino, Italy, and the Institute National Polytechnique de Lorraine, France.  He was a visitor scholar at the University of Pennsylvania and at Harvard’s CRCS center, and recipient of a EU Marie Curie Fellowship.  His research is in programming language design and implementation, and in differential privacy.

Faculty Host: Jan Hoffmann

Enumeration of graphs on surfaces (or "maps") is an active topic of research in combinatorics, with links to wide-ranging domains such as algebraic geometry, knot theory, and mathematical physics. In the last few years, it has also been found that map enumeration is related to the combinatorics of lambda calculus, with various well-known families of maps in 1-to-1 correspondence with various natural families of linear lambda terms. In the talk I will begin by giving a brief survey of these enumerative connections, then use those to motivate a closer look at the surprisingly rich topological and algebraic properties of linear lambda calculus.

Noam Zeilberger is a Birmingham Fellow in the School of Computer Science at the University of Birmingham. Previously, he held postdoctoral positions in France (Inria Saclay, Université Paris 7), Spain (IMDEA Madrid), and New Jersey (IAS Princeton), after receiving his PhD from CMU in 2009. He is interested in all aspects of logic and its interactions with mathematics and computer science.

Faculty Host: Robert Harper

In this talk, I will present my work on reasoning about concurrent programs with the Verified Software Toolchain (VST). Separation logic extends Hoare logic with ideas of memory and ownership, used to model the behavior of heap-manipulating programs. Permissions on memory are a natural way of thinking about both sequential and concurrent programs, but concurrency also brings its own challenges: how do threads communicate? Who owns a shared data structure? How can we account for relaxed memory models and low-level atomic operations?  Using ideas from the newest generation of concurrent separation logics, we can come up with consistent reasoning principles for both lock-based and lock-free programs, and prove the correctness of non-blocking communication protocols and data structures. These proofs are both formalized in Coq and connected to working C code.

William Mansky is a postdoc at Princeton University working with Andrew Appel on verifying concurrent C programs. He received his PhD from the University of Illinois at Urbana-Champaign under Elsa Gunter, and spent two years working with Steve Zdancewic on the Verified LLVM (Vellvm) project. His research interests include interactive theorem proving, program semantics and correctness, compiler correctness, and concurrency.

Faculty Host: Limin Jia

Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems.  A natural way to formalize program sensitivity is in terms of metrics on the input and output spaces, requiring that an r-sensitive function map inputs that are at distance d to outputs that are at distance at most r * d. Program sensitivity is thus an analogue of Lipschitz continuity for programs.  Reed and Pierce introduced Fuzz, a functional language with a linear type system that can express program sensitivity. They show soundness operationally, in the form of a metric preservation property.  Inspired by their work, we study program sensitivity and metric preservation from a   denotational point of view.  In particular, we introduce metric CPOs, a novel semantic structure for reasoning about computation on metric spaces, by endowing CPOs with a compatible notion of distance. This structure is useful for reasoning about metric properties of programs, and specifically about program sensitivity. We demonstrate metric CPOs by giving a model for the deterministic fragment of Fuzz.

Arthur Azevedo is graduate student in the Computer and Information Science department at the University of Pennsylvania since 2011. I work with Benjamin Pierce. My main research area is programming languages and verification. I was involved in the project of SAFE, a clean-slate computer environment aimed at security and correctness, helping with its design and specification. I am currently working on bringing some of the hardware tagging infrastructure that we developed for SAFE to more conventional processor designs, formally verifying that the mechanism can be used for enforcing interesting security policies.

Faculty Host: Jan Hoffmann

As capabilities, technology readiness and autonomy of unmanned aircraft matures, increasingly important aspects that come into consideration are these of correctness, failsafe-ness, robustness and health management. Furthermore, debugging and analysis of complex systems is an important part of development activities. Runtime monitoring of relevant properties and system requirements is a key technique to support such concepts. A suitable monitoring approach for a cyber-physical system has to be efficient and capable of supervising various specifications, possibly relating different data sources and data history. In this paper we present a formal approach for log-analysis and monitoring for the DLR ARTIS framework using a tool for the stream-based specification language LOLA, currently developed at Saarland University, for the runtime monitoring of formal specifications. The formal language is based on the concepts of linear temporal logic but is actually more expressive, for example it is possible to calculate probabilities instead of Boolean values. The formal methodology of runtime monitoring is introduced in the context of system health management, and application scenarios are detailed. The monitoring tool and its formal specification language LOLA is briefly described and the integration into the DLR ARTIS framework, phase one offline monitoring, and phase two online monitoring, is shown. Finally, examples show the benefits of using LOLA within the framework.

Florian-Michael Adolf has worked almost 15 years as a roboticist and got actively involved with many different challenges in perception, learning, planning and control. For example, he started working with camera-based object detection and autonomous transportation before he was working on real-time bision based soccer playing behaviors for a team of autonomous soccer robots (aka RoboCup). After he received my M.Sc. in Autonomous Systems in 2006, he specialized my research work in real-time sampling-based motion planning for unmanned rotocraft. Florian leads team of highly motivated researchers since 2013, who improve his initial work towards other unmanned aircraft types as well as the complex task of validation and verification thereof. Florian's daily work comprises not only technical and research work, but also international meetings with related special interest groups. But in order to keep his "feet on the ground", he tries to balance between theoretical and practical work as! well as related committee efforts. Through his work, he contributes to a better understanding as well as a feasibility analysis of approaches from various disciplines; i.e. an overall system perspective rather than a sole disciplinary one.

Sebastian Schirmer received his M.Sc. in Computer Science from Saarland University in 2016. During his studies as a research assistant he implemented the formal language LOLA that is used for monitoring approaches across different applications. With his thesis he achieved to augment athe unmanned rotorcraft guidance and control software framework with formal methods using LOLA. In particular, he applied monitoring to support the offline log-file analysis as well as online capabilities in order to enrich the information of the overall system states. This way he was able to analyze the system for assurance purposes "in-time". In 2017, he joined the German Aerospace Center (DLR) to continue working on Formal Methods and other Model-based assurance methods for unmanned aircraft.

Probabilistic couplings are a standard mathematical abstraction for reasoning about two distributions. In formal verification, they are often called probabilistic liftings. While these two concepts are quite related, the connection has been little explored. In fact, probabilistic couplings and liftings are a powerful, compositional tool for reasoning about probabilistic programs. I will give a brief survey of different uses of probabilistic liftings, and then show how to use these ideas in the relational program logic pRHL.

Joint with Gilles Barthe, Thomas Espitau, Benjamin Gregoire, and Pierre-Yves Strub.

Justin Hsu is a final year graduate student at the University of Pennsylvania, advised by Benjamin Pierce and Aaron Roth. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms, differential privacy, and game theory.

Faculty Host: Matt Fredrikson

It's tempting to think that machine instructions are atomic updates to a global mutable state, of register and memory values.  In the sequential world that's a good model, but concurrent contexts expose a slew of more interesting behaviour.  We set out to understand real multiprocessor semantics in 2007, to give a basis for software verification.  We're still not done, but we now have credible operational models for much of what goes on.  I'll talk about some key points of this, including our experimental investigation and validation, the Lem and Sail metalanguages for expressing the semantics, our interactions with processor vendors, especially IBM and ARM, and work with the CHERI team on secure hardware and software.  It's impacted hardware testing, architecture design, and high-level language design along the way.

This is part of the REMS project, aiming to apply semantics to improve the quality of mainstream computer systems; REMS also includes work on the C language and C/C++ concurrency model, on ELF linking, on POSIX filesystems,  on the TCP and TLS network and security protocols, on the CakeML verified compiler, and on program logics.   I'll start with a quick overview of REMS.

This is joint work with Shaked Flur, Susmit Sarkar, Kathryn E. Gray, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Ali Sezgin, Gabriel Kerneis, Dominic Mulligan, Anthony Fox, Robert Norton-Wright.

Peter Sewell is a Professor of Computer Science at the University of Cambridge Computer Laboratory.  He held an EPSRC Leadership Fellowship from 2010-2014 and a Royal Society University Research Fellowship from 1999-2007; he took his PhD in Edinburgh in 1995, supervised by Robin Milner, after studying in Cambridge and Oxford. His research aims to build rigorous foundations for the engineering of real-world computer systems, to make them better-understood, more robust, and more secure.

Faculty Host: Robert Harper

Rust is a new systems-programming language that is becoming increasingly popular. It aims to combine C++'s focus on zero-cost abstractions with numerous ideas that emerged first in academia, most notably affine and region types ("ownership and borrowing") and Haskell's type classes ("traits"). One of the key goals for Rust is that it does not require a garbage collector.

In this talk, I'll give a brief overview of Rust's key features, with a focus on the type system. I'll talk about how we leverage a few core features to offer a variety of APIs -- ranging from efficient collections to various styles of parallel programming -- while still guaranteeing memory safety and data-race freedom.

Nicholas Matsakis is a senior researcher at Mozilla research and a member of the Rust core team. He has been working on Rust for four years and did much of the initial work on its type system and other core features. He has also done work in several just-in-time compilers as well as building high-performance networking systems. He did his undergraduate study at MIT, graduating in 2001, and later obtained a PhD in 2011, working with Thomas Gross at ETH Zurich.

Faculty Host: Stephanie Balzer

Pages

Subscribe to POP