VSTTE 2023

15th International Conference on Verified Software: Theories, Tools, and Experiments

October 23-24, 2023, Ames, Iowa, USA
Co-located with Formal Methods in Computer-Aided Design 2023 (FMCAD 2023)

Submissions | Important Dates | Registration | Program | Invited Speakers | Invited Tutorial | Program Chairs | Program Committee | Previous Editions

Overview

The goal of the VSTTE conference series is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation.

The Verified Software Initiative (VSI), spearheaded by Tony Hoare and Jayadev Misra, is an ambitious research program for making large-scale verified software a practical reality. The International Conference on Verified Software: Theories, Tools and Experiments (VSTTE) is the main forum for advancing the initiative. VSTTE brings together experts spanning the spectrum of software verification in order to foster international collaboration on the critical research challenges. The theoretical work includes semantic foundations and logics for specification and verification, and verification algorithms and methodologies. The tools cover specification and annotation languages, program analyzers, model checkers, interactive verifiers and proof checkers, automated theorem provers and SAT/SMT solvers, and integrated verification environments. The experimental work drives the research agenda for theory and tools by taking on significant specification/verification exercises covering hardware, operating systems, compilers, computer security, parallel computing, and cyber-physical systems.

The 2023 edition of VSTTE will be the 15th international conference in the series, and will be co-located with FMCAD 2023 in Ames, Iowa, USA.

We welcome submissions describing significant advances in the production of verified software, i.e., software that has been proved to meet its functional specifications. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains. We are especially interested in submissions describing large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge. We also welcome papers describing novel experiments and case studies evaluating verification techniques and technologies.

Topics of interest for this conference include, but are not limited to, requirements modeling, specification languages, specification/verification/certification case studies, formal calculi, software design methods, automatic code generation, refinement methodologies, compositional analysis, verification tools (e.g., static analysis, dynamic analysis, model checking, theorem proving, satisfiability), tool integration, benchmarks, challenge problems, and integrated verification environments.

Paper Submissions

VSTTE 2023 will accept both long (limited to 16 pages, excluding references) and short (limited to 10 pages, excluding references) paper submissions. Short submissions also cover Verification Pearls describing an elegant proof or proof technique. Submitted research papers and system descriptions must be original and not submitted for publication elsewhere. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains.

Papers will be submitted via EasyChair at the VSTTE 2023 conference page. Submissions that arrive late, are not in the proper format, or are too long will not be considered. The post-conference proceedings of VSTTE 2023 will be published as a LNCS volume by Springer-Verlag. Authors of accepted papers will be requested to sign a form transferring copyright of their contribution to Springer-Verlag. The use of LaTeX and the Springer LNCS class files is strongly encouraged.

Important Dates

Registration

Registration to VSTTE will be part of the FMCAD registration process.

Program

Monday, October 23

8:00-8:25 Registration
8:25-8:30 Opening
Session 1
8:30-9:30 Invited speaker: Peter Mueller
Verified Secure Routing

Abstract: SCION is a new Internet architecture that addresses many of the security vulnerabilities of today’s Internet. Its clean-slate design provides, among other properties, route control, failure isolation, and multi-path communication. The verifiedSCION project is an effort to formally verify the correctness and security of SCION. It aims to provide strong guarantees for the entire architecture, from the protocol design to its concrete implementation. The project uses stepwise refinement to prove that the protocol withstands increasingly strong attackers. The refinement proofs assume that all network components such as routers satisfy their specifications. This property is then verified separately using deductive program verification in separation logic. This talk will give an overview of the verifiedSCION project and explain, in particular, how we verify code-level properties such as memory safety, I/O behavior, and information flow security.

Bio: Peter Müller has been Full Professor and head of the Programming Methodology Group at ETH Zurich since August 2008. His research focuses on languages, techniques, and tools for the development of correct software. His previous appointments include a position as Researcher at Microsoft Research in Redmond, an Assistant Professorship at ETH Zurich, and a position as Project Manager at Deutsche Bank in Frankfurt. Peter Müller received his PhD from the University of Hagen.

09:30-10:00 Joshua M. Cohen and Andrew W. Appel
Specifying and Verifying a Real-World Packet Error-Correction System
10:00-10:30 coffee break
Session 2
10:30-12:00 Invited tutorial: Mike Hicks
Cedar: A language for expressing fast, safe, and fine-grained authorization policies

Abstract: Cedar is a new authorization policy language developed as the core of AWS's recently released Amazon Verified Permissions (AVP) service. Cedar policies are used to express fine-grained permissions on behalf of applications. Cedar was designed to be ergonomic, fast, safe, and analyzable. Cedar’s simple and intuitive syntax supports common authorization use-cases with easy-to-understand policies. Cedar’s policy structure ensures that access requests can be authorized quickly. Cedar's policy validator leverages gradual typing to help policy writers avoid mistakes but not get in their way. Cedar's design has been finely balanced to enable a sound and complete logical encoding, which allows analysts to precisely reason about what policies do, e.g., to ensure that when refactoring a set of policies, the authorized permissions do not change. Cedar is built using a high-assurance process we call verification-guided development. Its authorization engine and validator are formally modeled in the Dafny programming language. Cedar’s core development team proves safety and security properties about those models in Dafny, and runs millions of automated differential tests to check that the implementations of the Cedar authorization engine and validator, written in Rust, agree with the Dafny models. Learn more about Cedar here and AVP here.

Bio: Mike Hicks is a Senior Principal Scientist at Amazon Web Services, and Professor Emeritus at the University of Maryland. His research explores programming languages and security. He is a Fellow of the Association of Computing Machinery (ACM), Editor-in-Chief of Proceedings of the ACM on Programming Languages, and prior Chair of ACM's Special Interest Group on Programming Languages. He co-leads the development of Cedar, the policy language underpinning the new Amazon Verified Permissions authorization service.

12:00-12:30 Marcus Rossel, Shaokai Lin, Marten Lohstroh, Jeronimo Castrillon and Andrés Goens
Provable Determinism for Software in Cyber-Physical Systems
12:30-14:00 lunch break
Session 3
14:00-15:00 Invited tutorial: Robert Jones
Solving in the Cloud, for the Cloud

Abstract: Deploying solvers at scale is both a challenge and an opportunity. The cloud provides an unprecedented volume of models to analyze, along with new requirements for solver performance, predictability, reliability, and correctness. The cloud also provides unprecedented scaling opportunities for concurrent solver computation. This talk discusses the science and engineering challenges associated with finding the right balance and suggests topics for further research.

Bio: Robert Jones is a Senior Principal Applied Scientist in Amazon’s Automated Reasoning Group. Prior to Amazon, Robert worked in hardware verification, modeling, prototyping, and security. He holds a PhD in Electrical Engineering from Stanford University. He enjoys reading, photography, playing the piano, being outside, and spending time with his family.

15:00-15:30 Konstantin Britikov, Natasha Sharygina and Antti Hyvärinen
Picky CDCL: SMT-solving With Flexible Literal Selection
15:30-16:00 Yakoub Nemouchi, Sriharsha Etigowni, Alexander Zolan and Richard Macwan
Formally verified ZTA requirements for OT/ICS environments with Isabelle/HOL
16:00-16:30 coffee break
Session 4
16:30-17:30 Invited talk: Arie Gurfinkel
Verifying Verified Code

Abstract: Bounded Model Checking (BMC) is an effective and precise static analysis technique that reduces program verification to satisfiability (SAT) solving. However, it is yet to be widely adopted in Industry. This talk describes our research on improving BMC usability through development of a new BMC engine (SeaBMC) in the SeaHorn verification framework for LLVM and through case studies on production code. Specifically, we report on our recent case study using Amazon Web Services aws-c-common library that was previously verified by CBMC. We also present the design and implementation of SeaBMC that precisely models arithmetic, pointer, and memory operations of LLVM. The key design innovation of SeaBMC is to structure verification condition generation around a series of transformations, starting with a custom IR (called SeaIR) that explicitly purifies all memory operations by explicating dependencies between them. This transformation-based approach enables supporting many different styles of verification conditions. To support memory safety checking, we extend our base approach with fat pointers and shadow bits of memory to keep track of metadata, such as the size of a pointed-to object. We show that SeaBMC can provide order of magnitude improvement compared with state-of-the-art.

Bio: Dr. Arie Gurfinkel is a Professor in the Department of Electrical and Computer Engineering at the University of Waterloo. He has published over 110 papers on automated verification. His research is in the areas of Program Analysis, Model Checking, and Automated Reasoning. His research group has led the implementation of award-winning program analysis framework SeaHorn, and award-winning solver for Constrained Horn Clauses, SPACER.

17:30-18:00 Chih-Hong Cheng, Harald Ruess and Konstantinos Theodorou
Safety Performance of Neural Networks in the Presence of Covariate Shift
18:00-18:30 Joseph Scott, Guanting Pan, Piyush Jha, Elias Khalil and Vijay Ganesh
Pierce: A Testing Tool for Neural Network Verification Solvers
18:30-18:35 Concluding Remarks by PC Chairs

Invited Speakers

Peter Mueller (ETHZ)

Title: Verified Secure Routing

Abstract: SCION is a new Internet architecture that addresses many of the security vulnerabilities of today’s Internet. Its clean-slate design provides, among other properties, route control, failure isolation, and multi-path communication. The verifiedSCION project is an effort to formally verify the correctness and security of SCION. It aims to provide strong guarantees for the entire architecture, from the protocol design to its concrete implementation. The project uses stepwise refinement to prove that the protocol withstands increasingly strong attackers. The refinement proofs assume that all network components such as routers satisfy their specifications. This property is then verified separately using deductive program verification in separation logic. This talk will give an overview of the verifiedSCION project and explain, in particular, how we verify code-level properties such as memory safety, I/O behavior, and information flow security.

Bio: Peter Müller has been Full Professor and head of the Programming Methodology Group at ETH Zurich since August 2008. His research focuses on languages, techniques, and tools for the development of correct software. His previous appointments include a position as Researcher at Microsoft Research in Redmond, an Assistant Professorship at ETH Zurich, and a position as Project Manager at Deutsche Bank in Frankfurt. Peter Müller received his PhD from the University of Hagen.

Arie Gurfinkel (U Waterloo)

Title: Verifying Verified Code

Abstract: Bounded Model Checking (BMC) is an effective and precise static analysis technique that reduces program verification to satisfiability (SAT) solving. However, it is yet to be widely adopted in Industry. This talk describes our research on improving BMC usability through development of a new BMC engine (SeaBMC) in the SeaHorn verification framework for LLVM and through case studies on production code. Specifically, we report on our recent case study using Amazon Web Services aws-c-common library that was previously verified by CBMC. We also present the design and implementation of SeaBMC that precisely models arithmetic, pointer, and memory operations of LLVM. The key design innovation of SeaBMC is to structure verification condition generation around a series of transformations, starting with a custom IR (called SeaIR) that explicitly purifies all memory operations by explicating dependencies between them. This transformation-based approach enables supporting many different styles of verification conditions. To support memory safety checking, we extend our base approach with fat pointers and shadow bits of memory to keep track of metadata, such as the size of a pointed-to object. We show that SeaBMC can provide order of magnitude improvement compared with state-of-the-art.

Bio: Dr. Arie Gurfinkel is a Professor in the Department of Electrical and Computer Engineering at the University of Waterloo. He has published over 110 papers on automated verification. His research is in the areas of Program Analysis, Model Checking, and Automated Reasoning. His research group has led the implementation of award-winning program analysis framework SeaHorn, and award-winning solver for Constrained Horn Clauses, SPACER.

Invited Tutorial

Mike Hicks (Amazon)

Title: Cedar: A language for expressing fast, safe, and fine-grained authorization policies

Abstract: Cedar is a new authorization policy language developed as the core of AWS's recently released Amazon Verified Permissions (AVP) service. Cedar policies are used to express fine-grained permissions on behalf of applications. Cedar was designed to be ergonomic, fast, safe, and analyzable. Cedar’s simple and intuitive syntax supports common authorization use-cases with easy-to-understand policies. Cedar’s policy structure ensures that access requests can be authorized quickly. Cedar's policy validator leverages gradual typing to help policy writers avoid mistakes but not get in their way. Cedar's design has been finely balanced to enable a sound and complete logical encoding, which allows analysts to precisely reason about what policies do, e.g., to ensure that when refactoring a set of policies, the authorized permissions do not change.

Cedar is built using a high-assurance process we call verification-guided development. Its authorization engine and validator are formally modeled in the Dafny programming language. Cedar’s core development team proves safety and security properties about those models in Dafny, and runs millions of automated differential tests to check that the implementations of the Cedar authorization engine and validator, written in Rust, agree with the Dafny models.

Learn more about Cedar here and AVP here.

Cedar is joint work with Craig Disselkoen, Aaron Eline, Shaobo He, Kesha Hietala, John Kastner, Anwar Mamat, Darin McAdams, Neha Rungta, Emina Torlak, and Andrew Wells (all at AWS).

Bio: Mike Hicks is a Senior Principal Scientist at Amazon Web Services, and Professor Emeritus at the University of Maryland. His research explores programming languages and security. He is a Fellow of the Association of Computing Machinery (ACM), Editor-in-Chief of Proceedings of the ACM on Programming Languages, and prior Chair of ACM's Special Interest Group on Programming Languages. He co-leads the development of Cedar, the policy language underpinning the new Amazon Verified Permissions authorization service.

Robert Jones (Amazon)

Title: Solving in the Cloud, for the Cloud

Abstract: Deploying solvers at scale is both a challenge and an opportunity. The cloud provides an unprecedented volume of models to analyze, along with new requirements for solver performance, predictability, reliability, and correctness. The cloud also provides unprecedented scaling opportunities for concurrent solver computation. This talk discusses the science and engineering challenges associated with finding the right balance and suggests topics for further research.

Bio: Robert Jones is a Senior Principal Applied Scientist in Amazon’s Automated Reasoning Group. Prior to Amazon, Robert worked in hardware verification, modeling, prototyping, and security. He holds a PhD in Electrical Engineering from Stanford University. He enjoys reading, photography, playing the piano, being outside, and spending time with his family.

General Chair

Program Chairs

Program Committee

Previous Editions