Powered by
11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2022),
June 14, 2022,
San Diego, CA, USA
11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2022)
Frontmatter
Welcome from the Chairs
Message from the Chairs
The 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP’22) is co-located with the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’22).
In line with past workshops, SOAP’22 aims to bring together the members of the program analysis community to share new developments and shape innovations in program analysis.
This edition of SOAP had nine submissions, each reviewed by three reviewers. Seven were accepted, making a ∼78% acceptance rate. Along with the accepted papers, SOAP’22 features three invited talks by leading members of the program analysis community: Elvira Albert (Complutense University of Madrid, Spain), Francesco Logozzo (META, Spain), and Caterina Urban (INRIA/ENS, France).
We would like to commend the efforts of the seven members of the program committee, who donated their valuable time and effort to make the reviewing process possible. We also thank the PLDI chairs and the ACM staff for their continued support in making this workshop possible. We hope you enjoy the talks at SOAP’22 and look forward to enlightening discussions.
Laure Gonnord
SOAP 2022 Program Co-Chair
Grenoble-INP/LCIS, France
Laura Titolo
SOAP 2022 Program Co-Chair
NIA/NASA LaRC, USA
Committees Program Chairs:
Laure Gonnord (Grenoble-INP/LCIS)
Laura Titolo (NIA/NASA LaRC, USA)
Program Committee:
Pietro Ferrara (Università Ca’ Foscari, Italy)
Carsten Fuhs (Birbeck/University of London, United Kingdom)
Isabel Garcia-Contreras (University of Waterloo, Canada)
François Gauthier (Oracle Labs, Australia)
Yannik Moy (AdaCore, France)
Jorge A. Navas (Certora, USA)
Julien Signoles (CEA LIST/University Paris-Saclay, France)
Steering Committee:
Padmanabhan Krishnan (Oracle Labs, Australia)
Christoph Reichenbach (Lund University, Sweden)
Neville Grech (University of Malta, Malta)
Thierry Lavoie (Synopsys, Canada)
Ben Hermann (Technische Universität Dortmund, Germany)
Omer Tripp (Amazon, USA)
Papers
BinFPE: Accurate Floating-Point Exception Detection for GPU Applications
Ignacio Laguna, Xinyi Li, and Ganesh Gopalakrishnan
(Lawrence Livermore National Laboratory, USA; University of Utah, USA)
When modern heterogeneous HPC systems perform numerical computations, floating-point exceptional quantities such as NaN and infinity in the GPU context, remain insufficiently handled. This is because commonly used GPUs and the CUDA language have no inherent exception detection capabilities. Existing compiler-based approaches for this problem are tied to a given compiler and cannot detect exceptions generated by binaries and precompiled libraries. This paper contributes BinFPE, a unique tool that addresses these challenges. BinFPE uses the NVBit dynamic binary instrumentation framework to check the machine registers after each calculation to recognize exceptions, and conveys this information to the CPU for final reporting. We demonstrate the effectiveness of BinFPE on 42 CUDA programs, reporting previously unreported exceptions. We also present the limitations of BinFPE and our perspective on building GPU tools via binary instrumentation.
@InProceedings{SOAP22p1,
author = {Ignacio Laguna and Xinyi Li and Ganesh Gopalakrishnan},
title = {BinFPE: Accurate Floating-Point Exception Detection for GPU Applications},
booktitle = {Proc.\ SOAP},
publisher = {ACM},
pages = {1--8},
doi = {10.1145/3520313.3534655},
year = {2022},
}
Publisher's Version
Modeling Code Manipulation in JIT Compilers
HeuiChan Lim, Xiyu Kang, and
Saumya Debray
(University of Arizona, USA)
Just-in-Time (JIT) compilers are widely used to improve the
performance of interpreter-based language implementations
by creating optimized code at runtime. However, bugs in
the JIT compiler’s code manipulation and optimization can
result in the generation of incorrect code. Such bugs can be
difficult to diagnose and fix, and can result in exploitable
vulnerabilities. Unfortunately, existing approaches to automatic
bug localization do not carry over well to such bugs.
This paper discusses a different approach to analyzing JIT
compiler optimization behaviors, based on using dynamic
analysis to construct abstract models of the JIT compiler’s
optimizer and back end. By comparing the models obtained
for buggy and non-buggy executions of the JIT compiler, we
can pinpoint the components of the JIT compiler’s internal
representation that have been affected by the bug; this can
then be mapped back to identify the buggy code. Our experiments
with two real bugs for Google V8 JIT compiler,
TurboFan, show the utility and practicality of our approach.
@InProceedings{SOAP22p9,
author = {HeuiChan Lim and Xiyu Kang and Saumya Debray},
title = {Modeling Code Manipulation in JIT Compilers},
booktitle = {Proc.\ SOAP},
publisher = {ACM},
pages = {9--15},
doi = {10.1145/3520313.3534656},
year = {2022},
}
Publisher's Version
Statically Detecting Data Leakages in Data Science Code
Pavle Subotić, Uroš Bojanić, and Milan Stojić
(Microsoft, Serbia)
Data leakage is a well-known problem in machine learning. Data leakage occurs when information from outside the training dataset is used to create a model. This phenomenon renders a model excessively optimistic or even useless in the real world since the model tends to leverage greatly on the unfairly acquired information. To date, detection of data leakages occurs post-mortem using runtime methods. In this paper, we develop a static data leakage analysis to detect several instances of data leakages during development time. Our analysis is constructed to be lightweight so that it can be performed within interactive data science notebooks. We have integrated our analysis into the NBLyzer static analyzer framework and show its utility on real world benchmarks. To the best of our knowledge, we propose the first static detection of data science data leakages.
@InProceedings{SOAP22p16,
author = {Pavle Subotić and Uroš Bojanić and Milan Stojić},
title = {Statically Detecting Data Leakages in Data Science Code},
booktitle = {Proc.\ SOAP},
publisher = {ACM},
pages = {16--22},
doi = {10.1145/3520313.3534657},
year = {2022},
}
Publisher's Version
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri,
Fabio Tagliaferro,
Vincenzo Arceri, Marco Ruaro,
Luca Negrini,
Agostino Cortesi,
Pietro Ferrara,
Fausto Spoto, and Enrico Talin
(University of Verona, Italy; Corvallis, Italy; Commercio.network, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy)
Ensuring determinism is mandatory when writing blockchain software.
When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes.
In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions.
However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes.
In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way.
Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes.
@InProceedings{SOAP22p23,
author = {Luca Olivieri and Fabio Tagliaferro and Vincenzo Arceri and Marco Ruaro and Luca Negrini and Agostino Cortesi and Pietro Ferrara and Fausto Spoto and Enrico Talin},
title = {Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report},
booktitle = {Proc.\ SOAP},
publisher = {ACM},
pages = {23--29},
doi = {10.1145/3520313.3534658},
year = {2022},
}
Publisher's Version
ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories
Md Rakib Hossain Misu, Aleksandar Saša Janjanin, Zhiqiang Bian, Valentin-Sebastian Burlacu, and Naum Anteski
(University College London, UK)
Writing highly maintainable and efficient software code is becoming increasingly difficult, especially while following the rapid, agile development process and working in a distributed team. One of the key indicators of that inefficient software design is a high degree of code coupling, which leads to unwanted side-effects during refactoring and acts as a burden during future development. To alleviate these problems, we developed a visualization tool, ADA, that statically analyzes an open-source repository and seeks to address the issue of code coupling by providing developers with a powerful graphic representation. ADA showcases the relationships and the degree of inter-connectivity between the classes. ADA will ultimately guide developers to instantly locate the coupled area and assist them in decoupling it.
@InProceedings{SOAP22p30,
author = {Md Rakib Hossain Misu and Aleksandar Saša Janjanin and Zhiqiang Bian and Valentin-Sebastian Burlacu and Naum Anteski},
title = {ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories},
booktitle = {Proc.\ SOAP},
publisher = {ACM},
pages = {30--35},
doi = {10.1145/3520313.3534659},
year = {2022},
}
Publisher's Version
Abstract Interpretation of Michelson Smart-Contracts
Guillaume Bau,
Antoine Miné, Vincent Botbol, and
Mehdi Bouaziz
(Sorbonne University, France; CNRS, France; LIP6, France; Nomadic Labs, France)
Static analysis of smart-contracts is becoming more widespread
on blockchain platforms. Analyzers rely on techniques
like symbolic execution or model checking, but few of them can
provide strong soundness properties and guarantee the analysis
termination at the same time. As smart-contracts often
manipulate economic assets, proving
numerical properties beyond the absence of runtime errors
is also desirable. Smart-contract
execution models differ considerably from mainstream
programming languages and vary from one blockchain to another,
making state-of-the-art analyses hard to adapt. For instance,
smart-contract calls may modify a persistent storage
impacting subsequent calls. This makes it difficult for tools to
infer invariants %and high-level security properties
required to formally ensure the absence of exploitable vulnerabilities.
The Michelson smart-contract language, used in the Tezos
blockchain, is strongly typed, stack-based, and has a strict
execution model leaving few opportunities
for implicit runtime errors. We present a work in progress static analyzer for Michelson
based on Abstract
Interpretation and implemented within MOPSA, a modular
static analyzer.
Our tool supports the Michelson semantic features, including inner calls to external
contracts. It can prove the absence of runtime errors and infer
invariants on the persistent storage over an unbounded number
of calls. It is also being extended to prove high-level
numerical and security properties.
@InProceedings{SOAP22p36,
author = {Guillaume Bau and Antoine Miné and Vincent Botbol and Mehdi Bouaziz},
title = {Abstract Interpretation of Michelson Smart-Contracts},
booktitle = {Proc.\ SOAP},
publisher = {ACM},
pages = {36--43},
doi = {10.1145/3520313.3534660},
year = {2022},
}
Publisher's Version
Archive submitted (8.2 kB)
Towards an Implementation of Differential Dynamic Logic in PVS
J. Tanner Slagel, César Muñoz, Swee Balachandran,
Mariano Moscato,
Aaron Dutle,
Paolo Masci, and
Lauren White
(NASA Langley Research Center, USA; National Institute of Aerospace, USA)
This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties.
@InProceedings{SOAP22p44,
author = {J. Tanner Slagel and César Muñoz and Swee Balachandran and Mariano Moscato and Aaron Dutle and Paolo Masci and Lauren White},
title = {Towards an Implementation of Differential Dynamic Logic in PVS},
booktitle = {Proc.\ SOAP},
publisher = {ACM},
pages = {44--50},
doi = {10.1145/3520313.3534661},
year = {2022},
}
Publisher's Version
proc time: 1.05