• root

• cv
• misc/

Sergei Stepanenko

Research Interests

I am interested in formal verification, programming language design, compilers, type systems, and functional programming. To date, I have contributed to the verification of an idealized model of hypervisors, the propositional semantics of generalized algebraic datatypes, and the denotational semantics of various types of continuation manipulations.

Projects

• Hypervisors
  Details

  
  High-level description
  We developed a simplified model of the Hafnium hypervisor and provided it with three elements:

  • A novel definition of weakest precondition that allows reasoning about assembly with cooperative concurrency.
  • Separation logic rules for Hafnium memory management instructions.
  • A logical relation to express “robust security”. With this, we were able to verify some examples where trusted code is linked with adversary code. By providing limited knowledge about the adversary code, we could still prove that the trusted code invariants are preserved.

  
  My contribution
  I have contributed to the definition of the hypervisor model, the separation logic rules for it, and the proof of the fundamental lemma.
• GADTs
  Details

  
  High-level description
  We provided a propositional model for a version of System F&omega with built-in equalities between types, allowing the expression of GADTs used in programming languages that support them (e.g., Haskell, OCaml). For this calculus, we provided the first propositional model using a novel technique that combines normalization by evaluation with logical relations. With this model, we were able to prove several things:

  • Combining impredicative polymorphism with injectivity of polymorphic types leads to a new encoding of non-terminating computation. Consequently, the language supporting them is not strongly normalizing even without effects or recursion.
  • Limited support of parametric reasoning about languages is possible even with syntactic constraints on types.
  • We were able to provide a few semantically correct but syntactically ill-typed programs and prove their properties.

  
  My contribution
  I have contributed to the definition of the semantic model, the proof of soundness of the language, and its extension to include effects such as state. This demonstrates that GADTs are orthogonal to additional computational language features.
• Guarded interaction trees
  Details

  
  High-level description
  I’m currently working on continuation-dependent effects. We extended Guarded Interaction Trees to allow effects that can observe or modify continuations around them. Using this extension, we provided a denotational semantics for a language with call/cc and for a language with shift/reset. Using that, we aim to provide denotational semantics to feature-rich languages, like OCaml with effect handlers, Scheme or SML with call/cc.
  My contribution
  In this project, I’ve been involved in modification of the original definition of reification for GITs, to allow them to capture continuation, thus, enabling reasoning about control-flow modification effects. To show that our approach is viable, I’ve provided a sound and adequate direct interpretation of a language with call/cc.
• Topos of trees formalization
  Details

  
  High-level description
  Formalization of the topos of trees, focusing on solving guarded domain equations over presheaves on ordinals, extending step-indexing techniques to transfinite settings. Prior work either handled a narrow class of functors or approached the problem abstractly using sheaves over complete Heyting algebras. We simplify this by working directly with presheaves, which are more suitable for mechanization. Our main contribution is a general solution for all guarded functors over presheaves on ordinals, along with its formalization in the Rocq proof assistant.
  My contribution
  Recursive domain equations solver, symmetrization, internal logic.
• Scheme embedded in Discord
  Details

  
  High-level description
  An extendable Scheme in Discord. Allows to easily extend the standard library by specifying wrappers for Discord-specific commands. This is just a toy project of mine that I really like.

Publications

• VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A PLDI 2023, Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, and Lars Birkedal
  Details

  
  Abstract
  Thin hypervisors make it possible to isolate key security components like keychains, fingerprint readers, and digital wallets from the easily-compromised operating system. To work together, virtual machines running on top of the hypervisor can make hypercalls to the hypervisor to share pages between each other in a controlled way. However, the design of such hypercall ABIs remains a delicate balancing task between conflicting needs for expressivity, performance, and security. In particular, it raises the question of what makes the specification of a hypervisor, and of its hypercall ABIs, good enough for the virtual machines. In this paper, we validate the expressivity and security of the design of the hypercall ABIs of Arm’s FF-A. We formalise a substantial fragment of FF-A as a machine with a simplified ISA in which hypercalls are steps of the machine. We then develop VMSL, a novel separation logic, which we prove sound with respect to the machine execution model, and use it to reason modularly about virtual machines which communicate through the hypercall ABIs, demonstrating the hypercall ABIs’ expressivity. Moreover, we use the logic to prove robust safety of communicating virtual machines, that is, the guarantee that even if some of the virtual machines are compromised and execute unknown code, they cannot break the safety properties of other virtual machines running known code. This demonstrates the intended security guarantees of the hypercall ABIs. All the results in the paper have been formalised in Coq using the Iris framework.
• The Essence of Generalized Algebraic Data Types POPL 2024, Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, and Lars Birkedal
  Details

  
  Abstract
  This paper considers direct encodings of generalized algebraic data types (GADTs) in a minimal suitable lambda-calculus. To this end, we develop an extension of System Fω with recursive types and internalized type equalities with injective constant type constructors. We show how GADTs and associated pattern-matching constructs can be directly expressed in the calculus, thus showing that it may be treated as a highly idealized modern functional programming language. We prove that the internalized type equalities in conjunction with injectivity rules increase the expressive power of the calculus by establishing a non-macro-expressibility result in Fω, and prove the system type-sound via a syntactic argument. Finally, we build two relational models of our calculus: a simple, unary model that illustrates a novel, two-stage interpretation technique, necessary to account for the equational constraints; and a more sophisticated, binary model that relaxes the construction to allow, for the first time, formal reasoning about data-abstraction in a calculus equipped with GADTs.
• Context-Dependent Effects in Guarded Interaction Trees To appear: ESOP 2025, Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, Lars Birkedal
  Details

  
  Abstract
  Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq. We present an extension of Guarded Interaction Trees to support formal reasoning about context-dependent effects. That is, effects which behavior depend on the evaluation context, e.g., call/cc, shift and reset. Using and reasoning about such effects is challenging since certain compositionality principles no longer hold in the presence of such effects. For example, the so-called ``bind rule’’ in modern program logics (which allows one to reason modularly about a term inside a context) is no longer valid. The goal of our extension is to support representation and reasoning about context-dependent effects in the most painless way possible. To that end, our extension is conservative: the reasoning principles (and the Coq implementation) for context-independent effects remain the same. We show that our implementation of context-dependent effects is viable and powerful. We use it to give direct-style denotational semantics for higher-order programming languages with call/cc and with delimited continuations. We extend the program logic for Guarded Interaction Trees to account for context-dependent effects, and we use the program logic to prove that the denotational semantics is adequate with respect to the operational semantics. This is achieved by constructing logical relations between syntax and semantics inside the program logic. Additionally, we retain the ability to combine multiple effects in a modular way, which we demonstrate by showing type soundness for safe interoperability of a programming language with delimited continuations and a programming language with higher-order store.

Talks

• The Essence of Generalized Algebraic Data Types, INRIA, 2023, Announcement
• The Essence of Generalized Algebraic Data Types, POPL, 2024, Slides

Community Service

• Committee Member in Artifact Evaluation Committee within the Research Artifacts-track, PLDI, 2024
• External reviewer, IJCAR, 2024

Teaching

• Compilation, TA, Fall 2021
• Distributed Systems and Security, TA, Fall 2022
• Computability and Logic, TA, Spring 2023
• Compilation, TA, Fall 2023
• Computer Architecture, Networks and Operating Systems, TA, Spring 2024, GDB notes

Links

• Short CV
• GitHub
• orcid