The Human Factors of Formal Methods (and Formal Methods Education)
Speaker: Tim Nelson
Tim Nelson is a senior lecturer in Computer Science at Brown University. Tim's research interests include lightweight formal methods and formal-methods education. Among other courses at Brown, he runs CSCI 1710 "Logic for Systems", which teaches lightweight formal methods by focusing on applications and tools. One example is Forge, a formal-methods tool that's built with teaching in mind. Before joining Brown, Tim worked as a software engineer and received his PhD from Worcester Polytechnic Institute, his B.S. from Worcester State College, and an A.A. from Diablo Valley College.
Abstract
As formal methods improve in expressiveness and power, they create new opportunities for non-expert adoption. In principle, formal tools are now powerful enough to enable developers to scalably validate realistic systems artifacts without extensive formal training. However, realizing this potential for adoption requires attention to not only the technical but also the human side—which has received extraordinarily little attention from formal-methods research.
This talk presents some of our efforts to address this paucity. We apply ideas from cognitive science, human-factors research, and education theory to improve the usability of formal methods. Along the way, we find misconceptions suffered by users, how technically appealing designs that experts may value may fail to help, and how our tools may even mislead users.
Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model
Speaker: Andrew Tolmach
Abstract
We propose a concrete (“pointer as integer”) memory semantics for C that supports verified compilation to a target environment having simple “public vs. private” data protection based on tagging or sandboxing (such as the WebAssembly virtual machine). Our semantics gives definition to a range of legacy programming idioms that cause undefined behavior in standard C, and are not covered by existing verified compilers, but that often work in practice. Compiler correctness in this context implies that target programs are secure against all control-flow attacks (although not against data-only attacks). To avoid tying our semantics too closely to particular compiler implementation choices, it is parameterized by a novel form of oracle that non-deterministically chooses the addresses of stack and heap allocations. As a proof-of-concept, we formalize a small RTL-like language and verify two-way refinement for a compiler from this language to a low-level machine and runtime system with hardware tagging. Our Coq formalization and proofs are provided as supplementary material.
This is joint work with Chris Chhak and Sean Anderson. The talk is a practice run a presentation at next month's Interactive Theorem Proving 2024 conference.
Expressive Policies for Microservice Networks
Speaker: Karuna Grewal
Karuna Grewal is a third year Ph.D. candidate in the Computer Science department at Cornell University advised by Prof. Justin Hsu. Her current research focus is to apply techniques from programming languages and formal methods to distributed and networked systems with a focus on security properties.
Abstract
Microservice-based application deployments need to administer safety properties while serving requests. However, today such properties can be specified only in limited ways that can lead to overly permissive policies and the potential for illegitimate flow of information across microservices, or ad hoc policy implementations.
We argue that a range of use cases require safety properties for the flow of requests across the whole microservice network, rather than only between adjacent hops. To begin specifying such expressive policies, we propose a system for declaring and deploying service tree policies. These policies are compiled down into declarative filters that are inserted into microservice deployment manifests. We use a light-weight dynamic monitor based enforcement mechanism, using ideas from automata theory. Experiments with our preliminary prototype show that we can capture a wide class of policies that we describe as case studies.
(This is a joint work with Brighten Godfrey from UIUC and Justin Hsu from Cornell University that appeared at HotNets'23.)
Discussing the Future of Quantum Programming Languages
Speaker: Benjamin C. A. Morrison
Benjamin C. A. Morrison is a Ph.D. student at the University of New Mexico and works in the Center for Computing Research at Sandia National Laboratories. They study quantum computing at all levels of the quantum software stack, from quantum programming languages to compilers, transpilers, error correction, quantum simulation algorithms, and occasionally complexity theory.
Abstract
Today’s quantum programming languages remain fairly rudimentary, with few exceptions. The core paradigm of “program as list of elementary operations” has been effective on testbed and small production quantum computers, but to scale up to larger systems we will want to support more sophisticated language constructs. I have some ideas on how to design such a language; I hope to share them with you, and hear your insights on how programming language theory can inform future quantum languages in turn. The views I will present are my own, and do not reflect those of the US Department of Energy or Sandia National Laboratories.
Why Arrows Matter?
Speaker: Yao Li
Abstract
I have recently been studying the concept of arrows in functional programming. Arrows were proposed by John Hughes in 1998 as a generalization of monads. They were later shown to be a structure whose expressiveness lies between applicative functors and monads. In this talk, I will share what I have learned so far. This talk assumes basic familiarity with functional programming, applicative functors, and monads.
Functional Logic Programming (programming by guess and check)
Speaker: Steven Libby
Dr. Libby is an internationally recognized researcher in the fields of functional logic programming, and functional logic compiler optimization. He is an assistant professor at the University of Portland where he teaches Programming Languages and Compilers. He is currently working on research, preparing for classes, and playing with his 2 cats, Timber and Lambda.
Abstract
Functional logic programming has recently gained a surge in popularity thanks to the Verse programming language. However, Verse didn't develop in a vacuum. The principles have been around for several decades. We will look at the Curry programming language and aim to answer the following questions: What is functional logic programming? Why should I care? and How does it work?