Workshop on Declarative Program AnalysisDPA 2018

The talk will discuss the general declarative points-to analysis approach of the Doop framework and then present some recent developments. The main emphasis will be on a defensive may-point-to analysis approach, which offers soundness even in the presence of arbitrary opaque code (e.g., reflection, dynamic loading, native code). It may be surprising that this goal is even achievable, so we will emphasize the unique architecture of the analysis and of its soundness guarantee.

Yannis Smaragdakis

University of Athens

Research Interests: programming languages and software engineering

• Program analysis (static analysis, test generation, invariant inference, symbolic execution)
• Language mechanisms for abstraction (declarative languages, program generation, DSLs, modules and components, generics, extensible languages, multi-paradigm programming)
• Languages and tools for systems (programming models for concurrency, language support for distributed computing, memory management and program locality)

CiaoPP is a context-sensitive, abstract interpretation-based analyzer and verifier based on transforming both high- and low-level program representations into Horn clauses and inferring via fixpoint computation the abstract semantics of such clauses, over a set of user-definable abstract domains. In this talk I will review the CiaoPP approach, and present recent applications such as energy consumption verification, static analysis of the cost of run-time checks for assertions, and some recent results in combining incremental and modular analysis.

Manuel Hermenegildo

IMDEA Software Institute and T.U. of Madrid (UPM)

Manuel Hermenegildo is a Full Professor and (Founding) Scientific Director of the IMDEA Software Institute. He is also a full Prof. of Computer Science at the Tech. U. of Madrid, UPM. Previously he held an Endowed Chair in Information Science and Technology at the U. of New Mexico. He was also project leader at the MCC research center and Adjunct Assoc. Prof. at the CS Department of the U. of Texas, both in Austin, Texas. See his home page for more information.

Research interests: Energy-Aware Computing, Resource / non-functional property analysis, verification, and control; Global Program Analysis, Optimization, Verification, Debugging; Abstract Interpretation; Partial Evaluation; Parallelism and Parallelizing Compilers; Constraint/Logic/Functional Programming Theory and Implementation, Abstract Machines; Automatic Documentation Tools, Execution Visualization; Sequential and Parallel Computer Architecture.

Program analyses detect errors in code but have to trade off precision, recall, and performance. However, when code changes frequently as in an IDE, repeated re-analysis from-scratch is unnecessary and leads to poor performance. Incremental program analysis promises to deliver fast feedback after a code change by deriving a new analysis result from the previous one, and prior work has shown that order-of-magnitude performance improvements are possible. However, existing frameworks for incremental program analysis only support Datalog-style relational analysis, but not lattice-based analyses that derive and aggregate lattice values. To solve this problem, we present the IncAL incremental program analysis framework that supports relational analyses and lattice-based computations. IncAL is based on a novel algorithm that enables the incremental maintenance of recursive lattice-value aggregation, which occurs when analyzing code with cyclic control flow by fixpoint iteration. To demonstrate our approach, we realized strong-update points-to analysis and string analyses for Java in IncAL and present performance measurements that demonstrate incremental analysis updates within milliseconds.

Tamás Szabó

itemis AG / TU Delft

Germany

Gábor Bergmann

Budapest University of Technology and Economics / MTA-BME Lendület Research Group on Cyber-Physical Systems

Hungary

Sebastian Erdweg

TU Delft

Netherlands

Markus Voelter

itemis

Ethereum is a distributed blockchain platform, serving as an ecosystem for smart contracts: full-fledged inter-communicating programs that capture the transaction logic of an account. Unlike programs in mainstream languages, the execution of an Ethereum smart contract is restricted by a gas limit: execution proceeds as long as gas is available. Thus, gas is a valuable resource that can be manipulated by an attacker to provoke unwanted behavior in a victim’s smart contract (e.g., wasting or blocking funds of said victim). Gas-focused vulnerabilities exploit undesired behavior when a contract (directly or through other interacting contracts) runs out of gas. Such vulnerabilities are among the hardest for programmers to protect against, as out-of-gas behavior may be uncommon in non-attack scenarios and reasoning about it is far from trivial.

In this paper, we classify and identify gas-focused vulnerabilities, and present MadMax: a static program analysis technique to automatically detect gas-focused vulnerabilities with very high confidence. Our approach combines a control-flow-analysis-based decompiler and declarative program-structure queries. The combined analysis captures high-level domain-specific concepts (such as “dynamic data structure storage” and “safely resumable loops”) and achieves high precision and scalability. MadMax analyzes the entirety of smart contracts in the current Ethereum blockchain in just 10 hours (with decompilation timeouts in 8% of the cases) and flags contracts with a current (though highly volatile) monetary value of over $5B as vulnerable. Manual inspection of a sample of flagged contracts shows that 81% of the sampled warnings do indeed lead to vulnerabilities, which we report on in our experiment.

Website

Link to Publication: http://www.nevillegrech.com/madmax-oopsla18.pdf

Neville Grech

University of Athens

Flix is a functional and logic language suited for the implementation of static analysis tools. Flix is inspired by Datalog and extends its semantics from constraints on relations to constraints on lattices. The key ingredients being the addition of user-defined lattices as well as monotone filter and transfer functions. This talk presents an overview of Flix, including recent progress made in ensuring the safety and soundness of program analyses written in Flix.

Magnus Madsen

Aalborg University

Denmark

I am an assistant professor at the Aalborg University, Aalborg, Denmark. I was previously a postdoctoral researcher at the University of Waterloo under the supervision of Ondřej Lhoták. I received my PhD from Aarhus University.

QL is an object-oriented dialect of Datalog that is particularly well suited for implementing program analyses in a high-level and declarative fashion. It forms the technical backbone of LGTM, which is Semmle’s engineering analytics platform for analysing projects written in a variety of languages, including C++, C#, Java, JavaScript and Python. LGTM not only provides insight into the current health of a code base by making static analysis alerts available to developers, but also shows how code quality has evolved over time, and how individual team members have contributed to it. In this talk, I will briefly introduce QL, concentrating on the features that make it a great tool for program analysis, and then take you on a tour of lgtm.com, a free instance of LGTM that continuously analyses all commits on over 70,000 open-source projects, and includes an in-browser IDE for writing your own QL queries.

Max Schaefer

Semmle

United Kingdom

I am a lead software engineer and engineering manager at Semmle Ltd. in Oxford, UK, where I mostly work on JavaScript analysis. Previously, I was an assistant professor at the School of Computer Engineering of Nanyang Technological University, Singapore; a post-doctoral researcher at IBM T.J. Watson Research Center, New York; and a PhD student at the Department of Computer Science at Oxford University.

Soufflé is a Datalog-based system for developing static analyses. It is currently being employed for industrial-strength static analysis problems (1) at Oracle Labs, where it is used as a rapid program analysis environment for security properties on the OpenJDK and (2) at Amazon Web Services, where it is used as a backend solver for a cloud security analysis tool.

A major challenge in such use cases is the ability to produce static analyses that are both customisable and scalable. While hand-crafted solutions (e.g., implemented in C++) have been shown to scale to large problem sizes, they lack the ability for users to easily define custom static analyses. Conversely, DSL-based analysers that are highly customisable, typically struggle to perform on a par with hand-crafted analysers.

In this talk I present Soufflé. Soufflé allows users to succinctly describe a static analysis via a highly flexible Datalog-based DSL and yet produce static analysers that exhibits the performance of state-of-the-art hand crafted tools. Soufflé has performed large scale static analyses typically deemed too difficult for Datalog-based solvers, including points-to analysis on the OpenJDK7 (1.4M program variables, 350K objects, 160K methods) in under a minute and security analysis of large Amazon VPC networks (10,000 Instances) in under 15 minutes.

This is joint work with Bernhard Scholz and Herbert Jordan.

Pavle Subotic

University College London

United Kingdom

We present a simple reductionist theory of lattices in a dialect of Datalog that is extended only with uninterpreted function symbols. We demonstrate three applications of the theory to monotonic aggregation, constant propagation, and the computation of graph dominators

Rei Thiessen

Google Inc.