Verification, model checking, and abstract interpretation

21st International Conference, VMCAI 2020

New Orleans, LA, USA, January 16–21, 2020

Proceedings

Verification, Model Checking,

LNCS 11990

and Abstract Interpretation

ARCoSS

Dirk Beyer

Damien Zufferey (Eds.)

Lecture Notes in Computer Science 11990

Founding Editors

Gerhard Goos, Germany

Juris Hartmanis, USA

Editorial Board Members

Elisa Bertino, USA

Wen Gao, China

Bernhard Steffen , Germany

Gerhard Woeginger , Germany

Moti Yung, USA

Advanced Research in Computing and Software Science

Subline of Lecture Notes in Computer Science

Subline Series Editors

Giorgio Ausiello, University of Rome ‘La Sapienza’, Italy

Vladimiro Sassone, University of Southampton, UK

Subline Advisory Board

Susanne Albers, TU Munich, Germany

Benjamin C. Pierce, University of Pennsylvania, USA

Bernhard Steffen, University of Dortmund, Germany

Deng Xiaotie, Peking University, Beijing, China

Jeannette M. Wing, Microsoft Research, Redmond, WA, USA

More information about this series at http://www.springer.com/series/7407

Dirk Beyer • Damien Zufferey (Eds.)

Verification, Model Checking,

and Abstract Interpretation

21st International Conference, VMCAI 2020

New Orleans, LA, USA, January 16–21, 2020

Proceedings

123

Editors

Dirk Beyer

Ludwig-Maximilians-Universität München

Munich, Germany

Damien Zufferey

Max Planck Institute for Software Systems

Kaiserslautern, Germany

ISSN 0302-9743 ISSN 1611-3349 (electronic)

Lecture Notes in Computer Science

ISBN 978-3-030-39321-2 ISBN 978-3-030-39322-9 (eBook)

https://doi.org/10.1007/978-3-030-39322-9

LNCS Sublibrary: SL1 – Theoretical Computer Science and General Issues

© Springer Nature Switzerland AG 2020

This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the

material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation,

broadcasting, reproduction on microfilms or in any other physical way, and transmission or information

storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now

known or hereafter developed.

The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication

does not imply, even in the absence of a specific statement, that such names are exempt from the relevant

protective laws and regulations and therefore free for general use.

The publisher, the authors and the editors are safe to assume that the advice and information in this book are

believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors

give a warranty, expressed or implied, with respect to the material contained herein or for any errors or

omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in

published maps and institutional affiliations.

This Springer imprint is published by the registered company Springer Nature Switzerland AG

The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

Preface

Welcome to VMCAI 2020, the 21st International Conference on Verification, Model

Checking, and Abstract Interpretation. VMCAI 2020 is part of the 47th

ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020),

at the hotel JW Marriott New Orleans, USA, during January 19–21, 2020.

Conference Description. VMCAI provides a forum for researchers from the

communities of verification, model checking, and abstract interpretation, facilitating

interaction, cross-fertilization, and advancement of hybrid methods that combine these

and related areas. The topics of the conference include program verification, model

checking, abstract interpretation, program synthesis, static analysis, type systems,

deductive methods, decision procedures, theorem proving, program certification,

debugging techniques, program transformation, optimization, and hybrid and

cyber-physical systems.

Focus on Reproducibility of Research Results. VMCAI 2020 included, for the

first time in this conference series, an optional artifact-evaluation (AE) process for

submitted papers. Reproducibility of results is of the utmost importance to the VMCAI

community. Therefore, we encouraged all authors to submit an artifact for evaluation.

An artifact is any additional material (software, data sets, machine-checkable proofs,

etc.) that substantiates the claims made in a paper and ideally makes them fully

replicable. The evaluation and archival of artifacts improves replicability and trace￾ability for the benefit of future research and the broader VMCAI community.

Paper Selection. VMCAI 2020 received a total of 44 paper submissions. After a

rigorous review process, with each paper reviewed by at least 3 Program Committee

(PC) members, followed by an online discussion, the PC accepted 21 full papers for

publication in the proceedings and presentation at the conference. The main selection

criteria were quality, relevance, and originality.

Invited Talks. The conference program includes three keynotes, by Rajeev Alur

(University of Pennsylvania, USA) on “Model Checking for Safe Autonomy,” Marta

Kwiatkowska (University of Oxford, UK) on “Safety and Robustness for Deep

Learning with Provable Guarantees,” and Moshe Vardi (Rice University, USA) on

“The Siren Song of Temporal Synthesis.”

Winter School. The VMCAI Winter School is the second winter school on formal

methods, associated with VMCAI 2020, New Orleans, USA, during January 16–18,

2020. In the vein of VMCAI, the school is meant to facilitate interaction,

cross-fertilization, and advancement of hybrid methods that combine verification,

model checking, and abstract interpretation. The school is aimed primarily at PhD

students who intend to continue their study in the field of verification.

The VMCAI Winter School program features lectures and tutorials from both aca￾demia and industry experts in their respective fields. The school covers several funda￾mental aspects of formal methods and applications. The following speakers were invited

to give lectures at the winter school: Dirk Beyer (Ludwig-Maximilians-Universität

München, Germany), Igor Konnov (Interchain Foundation, Switzerland), Marta

Kwiatkowska (University of Oxford, UK), Corina Pasareanu (NASA Ames and

Carnegie Mellon University, USA), Andreas Podelski (University of Freiburg,

Germany), Natasha Sharygina (University of Lugano, Switzerland), Helmut Seidl

(TU Munich, Germany), Moshe Vardi (Rice University, USA), Mike Whalen (Amazon

Web Services, USA), and Valentin Wüstholz (Consensys Diligence, Germany).

The venue of the second VMCAI Winter School is the New Orleans BioInnovation

Center. The school location and schedule was chosen to integrate nicely with POPL

and VMCAI, New Orleans, USA, during January 19–25, 2020. The registration for the

winter school was free but mandatory. As part of the registration, the applicants could

apply for travel and accommodation support, which we were able to provide thanks to

the generous donations of the sponsors. Furthermore, we helped to find room mates to

reduce the accommodation cost. Students with alternative sources of funding were also

welcome.

Artifact-Evaluation Process. For the first time, VMCAI 2020 used an AE process.

The goals of AE are: (1) getting more substantial evidence for the claims in the papers,

(2) simplify the replication of results in the paper, and (3) reward authors who create

artifacts. Artifacts are any additional material that substantiates the claims made in the

paper. Examples for artifacts are software, tools, frameworks, data sets, test suites, and

machine-checkable proofs.

Authors of submitted papers were encouraged to submit an artifact to the VMCAI

2020 Artifact-Evaluation Committee (AEC). We also encouraged the authors to make

their artifacts publicly and permanently available. Artifacts had to be provided as .zip

files and contain all necessary software for AE as well as a README file that describes

the artifact and provides instructions on how to replicate the results. AE had to be

possible in the VMCAI 2020 virtual machine, which runs an Ubuntu 19.04 with Linux

5.0.0-31 and was made publicly and permanently available on Zenodo1

.

All submitted artifacts were evaluated in parallel with the papers, and a meta-review

of the AE was provided to the reviewers of the respective papers. We assigned three

members of the AEC to each artifact and assessed it in two phases. First, the reviewers

tested if the artifacts were working, e.g., no corrupted or missing files exist and the

evaluation does not crash on simple examples. 5 of the 15 submitted artifacts passed the

first phase without any problems and we skipped the author clarification phase for

them. For the remaining 10 artifacts, we sent the issues of reviewers to the authors. The

authors’ answers to the reviewers were distributed among the reviewers, and the

authors were allowed to submit an updated artifact to fix issues found during the test

phase. In the second phase, the assessment phase, the reviewers aimed at replicating

any experiments or activities and evaluated the artifact based on the following five

questions:

1. Is the artifact consistent with the paper and the claims made by the paper?

2. Are the results of the paper replicable through the artifact?

3. Is the artifact complete, i.e., how many of the results of the paper are replicable?

1 https://doi.org/10.5281/zenodo.3533104

vi Preface

4. Is the artifact well-documented?

5. Is the artifact easy to use?

10 of the 15 submitted artifacts passed this second phase and were rewarded with the

‘Functional’ VMCAI AE badge. Independently, artifacts that are permanently and

publicly available were rewarded with the ‘Available’ VMCAI AE badge. 6 artifacts

received this ‘Available’ badge.

The VMCAI 2020 AEC consisted of the two chairs, Daniel Dietsch and

Marie-Christine Jakobs, and 20 committee members from 9 different countries.

Acknowledgments. We would like to thank, first of all, the authors for submitting

their papers to VMCAI 2020. The PC and the AEC did a great job of reviewing: they

contributed informed and detailed reports, and took part in the discussions during the

virtual PC meeting. We warmly thank the keynote speakers for their participation and

contributions. We also thank the general chair of the POPL 2020 week, Brigitte

Pientka, and her team for the overall organization. We thank Alfred Hofmann and his

publication team at Springer-Verlag for their support, and EasyChair for providing an

excellent review system. Special thanks goes to the VMCAI Steering Committee, and

in particular to Lenore Zuck, Ruzica Piskac, and Andreas Podelski, for their helpful

advice, assistance, and support.

Last but not least, we thank the sponsors of the VMCAI winter school —Amazon

Web Services, Moloch DAO/Consensys Diligence, Interchain, Cadence, and

Springer— for their financial contributions to supporting the winter school for students.

December 2019 Dirk Beyer

Damien Zufferey

PC Chairs

Daniel Dietsch

Marie-Christine Jakobs

AEC Chairs

Preface vii

Organization

Program Committee

Dirk Beyer (PC Chair) LMU Munich, Germany

Damien Zufferey (PC Chair) MPI, Germany

Timos Antonopoulos Yale University, USA

Nikolaj Bjorner Microsoft, USA

Pavol Cerny University of Colorado Boulder, USA

Rayna Dimitrova University of Leicester, UK

Constantin Enea IRIF and Université Paris Diderot, France

Pierre Ganty IMDEA Software Institute, Spain

Alberto Griggio Fondazione Bruno Kessler, Italy

Ashutosh Gupta TIFR, India

Marie-Christine Jakobs TU Darmstadt, Germany

Laura Kovacs Vienna University of Technology, Austria

Jan Kretinsky TU Munich, Germany

Markus Kusano Google, USA

Ori Lahav Tel Aviv University, Israel

David Monniaux CNRS and VERIMAG, France

Kedar Namjoshi Bell Labs, USA

Andreas Podelski University of Freiburg, Germany

Nadia Polikarpova UC San Diego, USA

Shaz Qadeer Facebook, USA

Daniel Schwartz-Narbonne Amazon Web Services, USA

Martina Seidl Johannes Kepler University Linz, Austria

Natasha Sharygina USI Lugano, Switzerland

Mihaela Sighireanu IRIF, CNRS, and Université Paris Diderot, France

Jan Strejček Masaryk University, Czechia

Alexander J. Summers ETH Zurich, Switzerland

Michael Tautschnig Queen Mary University of London and AWS, UK

Caterina Urban Inria, France

Heike Wehrheim University of Paderborn, Germany

Thomas Wies New York University, USA

Lenore Zuck University of Illinois in Chicago, USA

Artifact Evaluation Committee (AEC)

Daniel Dietsch (AEC Chair) University of Freiburg, Germany

Marie-Christine Jakobs

(AEC Chair)

TU Darmstadt, Germany

Aleš Bizjak Aarhus University, Germany

Martin Bromberger MPI-INF, Germany

Maryam Dabaghchian University of Utah, USA

Simon Dierl TU Dortmund, Germany

Rayna Dimitrova University of Leicester, UK

Mathias Fleury MPI-INF, Germany

Ákos Hajdu Budapest University of Technology and Economics,

Hungary

Marcel Hark RWTH Aachen University, Germany

Ben Hermann Paderborn University, Germany

Christian Herrera fortiss GmbH, Germany

Martin Jonáš Fondazione Bruno Kessler, Italy

Bishoksan Kafle University of Melbourne, Australia

Martin Kellogg University of Washington Seattle, USA

Sven Linker University of Liverpool, UK

Alessio Mansutti CNRS, LSV, and ENS Paris-Saclay, France

Marco Muñiz Aalborg University, Denmark

Yannic Noller Humboldt-Universität zu Berlin, Germany

Kostiantyn Potomkin Australian National University, Australia

Christian Schilling IST Austria, Austria

Martin Spießl LMU Munich, Germany

Steering Committee

Andreas Podelski

(SC Chair)

University of Freiburg, Germany

Tino Cortesi Università Ca’ Foscari Venezia, Italy

Patrick Cousot New York University, USA

Ruzica Piskac Yale University, USA

Lenore Zuck UIC, USA

Additional Reviewers

Asadi, Sepideh

Ashok, Pranav

Basset, Nicolas

Beillahi, Sidi Mohamed

Blicha, Martin

Chalupa, Marek

Chatterjee, Krishnendu

Chen, Yu-Ting

Chevalier, Marc

Dohrau, Jérôme

Eilers, Marco

Eisentraut, Julia

Genaim, Samir

Guo, Zheng

Haltermann, Jan

Hyvärinen, Antti

Janota, Mikoláš

Kröger, Paul

König, Jürgen

Lewchenko, Nicholas

Magnago, Enrico

Marescotti, Matteo

Meggendorfer, Tobias

Mutluergil, Suha Orhun

Obdržálek, Jan

Oortwijn, Wytse

Rabe, Markus N.

Raskin, Jean-Francois

x Organization

Reynolds, Andrew

Richter, Cedric

Roveri, Marco

Sallinger, Sarah

Schneidewind, Clara

Schwerhoff, Malte

Toews, Manuel

Unadkat, Divyesh

van Dijk, Tom

Organization xi

Contents

Witnessing Secure Compilation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

Kedar S. Namjoshi and Lucas M. Tabajara

BackFlow: Backward Context-Sensitive Flow Reconstruction of Taint

Analysis Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

Pietro Ferrara, Luca Olivieri, and Fausto Spoto

Fixing Code that Explodes Under Symbolic Evaluation . . . . . . . . . . . . . . . . 44

Sorawee Porncharoenwase, James Bornholt, and Emina Torlak

The Correctness of a Code Generator for a Functional Language . . . . . . . . . 68

Nathanaël Courant, Antoine Séré, and Natarajan Shankar

Leveraging Compiler Intermediate Representation

for Multi- and Cross-Language Verification . . . . . . . . . . . . . . . . . . . . . . . . 90

Jack J. Garzella, Marek Baranowski, Shaobo He,

and Zvonimir Rakamarić

Putting the Squeeze on Array Programs: Loop Verification via Inductive

Rank Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112

Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham

A Systematic Approach to Abstract Interpretation

of Program Transformations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136

Sven Keidel and Sebastian Erdweg

Sharing Ghost Variables in a Collection of Abstract Domains. . . . . . . . . . . . 158

Marc Chevalier and Jérôme Feret

Harnessing Static Analysis to Help Learn Pseudo-Inverses of String

Manipulating Procedures for Automatic Test Generation . . . . . . . . . . . . . . . 180

Oren Ish-Shalom, Shachar Itzhaky, Roman Manevich,

and Noam Rinetzky

Synthesizing Environment Invariants for Modular Hardware Verification . . . . 202

Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta,

and Sharad Malik

Systematic Classification of Attackers via Bounded Model Checking. . . . . . . 226

Eric Rothstein-Morris, Jun Sun, and Sudipta Chattopadhyay

Cheap CTL Compassion in NuSMV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 248

Daniel Hausmann, Tadeusz Litak, Christoph Rauch,

and Matthias Zinner

A Cooperative Parallelization Approach for Property-Directed k-Induction . . . 270

Martin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti,

and Natasha Sharygina

Generalized Property-Directed Reachability for Hybrid Systems . . . . . . . . . . 293

Kohei Suenaga and Takuya Ishizawa

Language Inclusion for Finite Prime Event Structures . . . . . . . . . . . . . . . . . 314

Andreas Fellner, Thorsten Tarrach, and Georg Weissenbacher

Promptness and Bounded Fairness in Concurrent

and Parameterized Systems. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 337

Swen Jacobs, Mouhammad Sakr, and Martin Zimmermann

Solving LIAH Using Approximations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 360

Maxwell Levatich, Nikolaj Bjørner, Ruzica Piskac, and Sharon Shoham

Formalizing and Checking Multilevel Consistency. . . . . . . . . . . . . . . . . . . . 379

Ahmed Bouajjani, Constantin Enea, Madhavan Mukund,

Gautham Shenoy R., and S. P. Suresh

Practical Abstractions for Automated Verification

of Shared-Memory Concurrency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 401

Wytse Oortwijn, Dilian Gurov, and Marieke Huisman

How to Win First-Order Safety Games . . . . . . . . . . . . . . . . . . . . . . . . . . . 426

Helmut Seidl, Christian Müller, and Bernd Finkbeiner

Improving Parity Game Solvers with Justifications . . . . . . . . . . . . . . . . . . . 449

Ruben Lapauw, Maurice Bruynooghe, and Marc Denecker

Author Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 471

xiv Contents

Witnessing Secure Compilation

Kedar S. Namjoshi1(B) and Lucas M. Tabajara2

1 Nokia Bell Labs, Murray Hill, NJ, USA

[email protected]

2 Rice University, Houston, TX, USA

[email protected]

Abstract. Compiler optimizations may break or weaken the security

properties of a source program. This work develops a translation valida￾tion methodology for secure compilation. A security property is expressed

as an automaton operating over a bundle of program traces. A refinement

proof scheme derived from a property automaton guarantees that the

associated security property is preserved by a program transformation.

This generalizes known refinement methods that apply only to specific

security properties. In practice, the refinement relations (“security wit￾nesses”) are generated during compilation and validated independently

with a refinement checker. This process is illustrated for common opti￾mizations. Crucially, it is not necessary to formally verify the compiler

implementation, which is infeasible for production compilers.

1 Introduction

Optimizing compilers are used to improve the run time performance of soft￾ware programs. An optimization is correct if it preserves input-output behavior.

A number of approaches, including automated testing (cf. [13,28]), translation

validation (cf. [22,25,31]), and full mathematical proof (cf. [14]) have been devel￾oped to gain confidence in the correctness of compilation.

Correctness does not, however, guarantee the preservation of security prop￾erties. It is known that common optimizations may weaken or break security

properties that hold of a source program (cf. [10,12]). A secure compiler is one

that, in addition to being correct, also preserves security properties. This work

provides a methodology for formally establishing secure compilation.

int x := read_secret_key();

use(x);

x := 0; // clear secret data

rest_of_program();

int x := read_secret_key();

use(x);

skip; // dead store removed

rest_of_program();

Fig. 1. Information leakage through optimization. Source program on left, optimized

program on right.

c Springer Nature Switzerland AG 2020

D. Beyer and D. Zufferey (Eds.): VMCAI 2020, LNCS 11990, pp. 1–22, 2020.

https://doi.org/10.1007/978-3-030-39322-9_1

2 K. S. Namjoshi and L. M. Tabajara

Figure 1 shows an instance of the dead store removal optimization. This opti￾mization eliminates stores (i.e., assignment statements) that have no effect on

the input-output behavior of the source program. If variable x is not referenced

in rest_of_program, the optimization correctly replaces x := 0 with skip. The

replacement, however, exposes the secret key stored in x to the rest of the pro￾gram, which may be vulnerable to an attack that leaks this secret, thus breaking

a vital security property of the source program.

Compiler directives can be used to prevent this optimization from taking

effect. Such fixes are unsatisfactory and brittle, however, as they assume that

programmers are aware of the potential security issue and understand enough

of a compiler’s workings to choose and correctly place the directives. Moreover,

the directives may not be portable across compilers [29].

It is far more robust to build security preservation into a compiler. The clas￾sical approach constructs a mathematical proof of secure compilation, applicable

to all source programs. This is highly challenging for at least two reasons. The

first is that of proof complexity. Past experience shows that such proofs can

take man-years of effort, even for compact, formally designed compilers such as

CompCert [4,14]. Constructing such proofs is entirely infeasible for production

compilers such as GCC or LLVM, which have millions of lines of code written in

hard-to-formalize languages such as C and C++. The second reason is that, unlike

correctness, secure compilation is not defined by a single property: each source

program may have its own notion of security. Even standard properties such as

non-interference and constant-time have subtle variants.

This work addresses both issues. To tackle the issue of proof complexity, we

turn to Translation Validation [25] (TV), where correctness is established at

compile time only for the program being compiled. We use a form of TV that we

call “witnessing” [21,26], where a compiler is designed to generate a proof (also

called a “certificate” or a “witness”) of property preservation. For correctness

properties, this proof takes the form of a refinement relation relating single traces

of source and target programs. For security preservation, it is necessary to have

refinement relations that relate “bundles” of k traces (k ≥ 1) from the source

and target programs.

To address the second issue, we show how to construct property-specific

refinement proof rules. A security property is defined as an automaton operat￾ing on trace bundles, a flexible formulation that encompasses standard security

properties such as non-interference and constant-time. The shape of the induced

refinement proof rule follows the structure of the property automaton.

Refinement rules are known for the important security properties of non￾interference [3,8,17] and constant-time execution [4]. We show that these rules

arise easily and directly from an automaton-based formulation. As automata

can express a large class of security properties, including those in the HyperLTL

logic [6], the ability to derive refinement proof rules from automata considerably

expands the reach of the refinement method.

We now discuss these contributions in more detail. We use a logic akin to

HyperLTL [6] to describe security hyperproperties [7,27], which are sets of sets