Powered by
23rd ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2021),
July 13, 2021,
Virtual, Denmark
23rd ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2021)
Frontmatter
Welcome from the Chair
Welcome to the 23rd Workshop on Formal Techniques for Java-like Programs (FTfJP 2021), which is co-located with ECOOP and ISSTA 2021 and held virtually on July 13, 2021.
Papers
Source Code Patches from Dynamic Analysis
Indigo Orton and
Alan Mycroft
(University of Cambridge, UK)
Dynamic analysis can identify improvements to programs that cannot feasibly be identified by static analysis; concurrency improvements are a motivating example. However, mapping these dynamic-analysis-based improvements back to patch-like source-code changes is non-trivial. We describe a system, Scopda, for generating source-code patches for improvements identified by execution-trace-based dynamic analysis. Scopda uses a graph-based static program representation (abstract program graph, APG), containing inter-procedural control flow and local data flow information, to analyse and transform static source-code. We demonstrate Scopda's ability to generate sensible source code patches for Java programs, though it is fundamentally language agnostic.
@InProceedings{FTfJP21p1,
author = {Indigo Orton and Alan Mycroft},
title = {Source Code Patches from Dynamic Analysis},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {1--8},
doi = {10.1145/3464971.3468416},
year = {2021},
}
Publisher's Version
A Generic Type System for Featherweight Java
Ulrich Schöpp and
Chuangjie Xu
(fortiss, Germany)
We introduce a generic type system for Featherweight Java (FJ) that is parametrized with a monad-like structure, and prove a uniform soundness theorem. Its instances include some region type systems studied by Martin Hofmann et al. as well as a new one that performs more precise analysis of trace-based properties. Their soundness is guaranteed by the uniform theorem. We only need to verify some natural conditions. Instead of refining the FJ type system as in the previous work, our region type system is separate from the FJ type system, making it simpler and also easier to move to larger fragments of Java. Moreover, the uniform framework helps to avoid redundant work on the meta-theory when extending the system to cover other language features such as exception handling.
@InProceedings{FTfJP21p9,
author = {Ulrich Schöpp and Chuangjie Xu},
title = {A Generic Type System for Featherweight Java},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {9--15},
doi = {10.1145/3464971.3468419},
year = {2021},
}
Publisher's Version
Refactoring Traces to Identify Concurrency Improvements
Indigo Orton and
Alan Mycroft
(University of Cambridge, UK)
It is often difficult to analyse why a program executes more slowly than intended. This is particularly true for concurrent programs. We describe and evaluate a system, Rehype, which takes Java programs, performs low-overhead tracing of method calls, analyses the resulting trace-logs to detect inefficient uses of concurrency constructs, and suggests source-code-oriented improvements. Rehype deals with task-based concurrency, specifically a future-based model of tasks. Implementing the suggested improvements on an industrial API server more than doubled request-processing throughput.
@InProceedings{FTfJP21p16,
author = {Indigo Orton and Alan Mycroft},
title = {Refactoring Traces to Identify Concurrency Improvements},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {16--23},
doi = {10.1145/3464971.3468420},
year = {2021},
}
Publisher's Version
Reconstructing Z3 Proofs in KeY: There and Back Again
Wolfram Pfeifer,
Jonas Schiffl, and
Mattias Ulbrich
(KIT, Germany)
One of the main factors of the increasing power of deductive verification tools are modern SMT solvers. Unfortunately, SMT solvers usually do not produce proof artifacts that could be inspected or checked. KeY is a formal platform for the deductive verification of Java programs which produces explicit, browsable proofs. SMT solvers can be driven from within KeY, but this unfortunately breaks these proof transparency intentions.
In this paper, we describe how we complemented the existing translation of proof obligations to Z3 (There ...) with the replay of proof transcripts reported by Z3 inside KeY (... and Back Again). We describe the conceptual and engineering challenges we encountered for this round trip and present solutions for them.
The replay technique has been implemented in KeY, and in the evaluation, we demonstrate the feasibility of the approach for first-order proof instances and investigate the effects of proof replay on the proof run time and size.
@InProceedings{FTfJP21p24,
author = {Wolfram Pfeifer and Jonas Schiffl and Mattias Ulbrich},
title = {Reconstructing Z3 Proofs in KeY: There and Back Again},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {24--31},
doi = {10.1145/3464971.3468421},
year = {2021},
}
Publisher's Version
Using Dafny to Solve the VerifyThis 2021 Challenges
Marie Farrell,
Conor Reynolds, and
Rosemary Monahan
(Maynooth University, Ireland)
This paper provides an experience report of using the Dafny program verifier, at the VerifyThis 2021 program verification competition. The competition aims to evaluate the usability of logic-based program verification tools in a controlled experiment, challenging both the verification tools and the users of those tools. We present the two challenges that we tackled during the competition and discuss our solutions. As a result, we identify strengths and weaknesses of Dafny in the verification of relatively complex algorithms, and report on our experience of applying Dafny in this setting.
@InProceedings{FTfJP21p32,
author = {Marie Farrell and Conor Reynolds and Rosemary Monahan},
title = {Using Dafny to Solve the VerifyThis 2021 Challenges},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {32--38},
doi = {10.1145/3464971.3468422},
year = {2021},
}
Publisher's Version
IntelliJML: A JML Plugin for IntelliJ IDEA
Steven Monteiro, Erikas Sokolovas, Ellen Wittingen,
Tom van Dijk, and
Marieke Huisman
(University of Twente, Netherlands)
Java code can be annotated with formal specifications using the Java Modelling Language (JML). Previous work has provided IDE plugins intended to help write JML, but mostly for the Eclipse IDE. We introduce IntelliJML, a JML plugin for IntelliJ IDEA, with a focus on ease of use and maintainability. Features such as syntax, semantic, and type checking, as well as syntax highlighting and code completion are integrated into the plugin. The plugin can also be extended in the future to add more features. The source code for the plugin can be found at https://gitlab.utwente.nl/fmt/intellijml.
@InProceedings{FTfJP21p39,
author = {Steven Monteiro and Erikas Sokolovas and Ellen Wittingen and Tom van Dijk and Marieke Huisman},
title = {IntelliJML: A JML Plugin for IntelliJ IDEA},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {39--42},
doi = {10.1145/3464971.3468423},
year = {2021},
}
Publisher's Version
Info
Ensuring Correct Cryptographic Algorithm and Provider Usage at Compile Time
Weitian Xing, Yuanhui Cheng, and
Werner Dietl
(University of Waterloo, Canada)
Using cryptographic APIs to encrypt and decrypt data, calculate digital signatures, or compute hashes is error prone. Weak or unsupported cryptographic algorithms can cause information leakage and runtime exceptions, such as a NoSuchAlgorithmException in Java. Using the wrong cryptographic service provider can also lead to unsupported cryptographic algorithms. Moreover, for Android developers who want to store their key material in the Android Keystore, misused cryptographic algorithms and providers make the key material unsafe.
We present the Crypto Checker, a pluggable type system that detects the use of forbidden algorithms and providers at compile time. For typechecked code, the Crypto Checker guarantees that only trusted algorithms and providers are used, and thereby ensures that the cryptographic APIs never cause runtime exceptions or use weak algorithms or providers. The Crypto Checker is easy-to-use: it allows developers to determine which algorithms and providers are permitted by writing specifications using type qualifiers.
We implemented the Crypto Checker for Java and evaluated it with 32 open-source Java applications (over 2 million LOC). We found 2 issues that cause runtime exceptions and 62 violations of security recommendations and best practices. We also used the Crypto Checker to analyze 65 examples from a public benchmark of hard security issues and discuss the differences between our approach and a different static analysis in detail.
@InProceedings{FTfJP21p43,
author = {Weitian Xing and Yuanhui Cheng and Werner Dietl},
title = {Ensuring Correct Cryptographic Algorithm and Provider Usage at Compile Time},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {43--50},
doi = {10.1145/3464971.3468418},
year = {2021},
}
Publisher's Version
Behavioural Separation with Parallel Usages
Iaroslav Golovanov,
Hans Hüttel,
Mathias Jakobsen, and Mikkel Kettunen
(Aalborg University, Denmark; University of Glasgow, UK)
Mungo is an object-oriented language that uses typestates with a behavioural type system to ensure the absence of null-dereferencing. Typestates are usages that specify the admissible sequences of method calls on objects. Previous type systems for Mungo have all had a linearity constraint on objects. We present an extension of these systems, where usage specifications can now include a parallel construct that lets us describe separate local behaviour. A parallel usage describes a separation of the heap, and this allows us to reason about aliasing and to express arbitrary interleaving of local protocols. This also solves the state-space explosion problem for usages. Our extension retains the safety properties of previous type systems for Mungo.
@InProceedings{FTfJP21p51,
author = {Iaroslav Golovanov and Hans Hüttel and Mathias Jakobsen and Mikkel Kettunen},
title = {Behavioural Separation with Parallel Usages},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {51--58},
doi = {10.1145/3464971.3468424},
year = {2021},
}
Publisher's Version
Combining Formal and Machine Learning Techniques for the Generation of JML Specifications
Armand Puccetti,
Gaël de Chalendar, and
Pierre-Yves Gibello
(University of Paris-Saclay, France; CEA LIST, France; OW2, France)
Producing maintainable programs is a big challenge for the
software industry as it requires solid Engineering skills and
efficient CASE tools. Often, industrial programs are of a very large
size (more than 1M SLOC), use high-level programming languages
to their full extent (e.g. C++20, Ada 2005 or Java 16), are provided
with scarce and often outdated documentation partially written in
natural language. Maintenance engineers are therefore in need to
understand the application at hand starting from the material left
behind by the developers.
The European H2020 Project DECODER (https://www.decoder-
project.eu) addresses this problem by proposing to combine
Natural Language Processing techniques and Formal Methods to
turn as best as possible code artifacts into formal data allowing to
reduce the maintenance costs and thus the total costs of
ownership.
In this context, we will show how to generate JML annotations
using a combination of 1) automatic generation of minimal
predicates, 2) Natural Language Processing (NLP) based predicates
generator, and 3) manual refinement and correction, to instrument
and enhance code and documentation. We will illustrate it on code
samples from the MyThaiStar (https://github.com/devonfw/my-
thai-star) application developed with the CASE tool devonfw by
CAP GEMINI, and the Joram JMS implementation
(https://gitlab.ow2.org/joram/joram) from OW2 code base.
@InProceedings{FTfJP21p59,
author = {Armand Puccetti and Gaël de Chalendar and Pierre-Yves Gibello},
title = {Combining Formal and Machine Learning Techniques for the Generation of JML Specifications},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {59--64},
doi = {10.1145/3464971.3468425},
year = {2021},
}
Publisher's Version
JML and OpenJML for Java 16
David R. Cok
(Safer Software Consulting, USA)
As the Java language evolves, the Java Modeling Language (JML) and the OpenJML deductive verification tool must evolve with it.
Changes in Java since Java 8 bring language and organizational changes which affect the semantics of JML and the implementation of OpenJML. They also raise questions about language definition, joint efforts, and community engagement, some enumerated in this paper, for the Java formal reasoning community to address.
@InProceedings{FTfJP21p65,
author = {David R. Cok},
title = {JML and OpenJML for Java 16},
booktitle = {Proc.\ FTfJP},
publisher = {ACM},
pages = {65--67},
doi = {10.1145/3464971.3468417},
year = {2021},
}
Publisher's Version
proc time: 1.54