Objective

In the last ten years, a wide range of static analysis tools have emerged, some of which are currently in industrial use or are well beyond the advanced prototype level. Many impressive practical results have been obtained, which allow complex properties to be proven or checked in a fully or semi-automatic way, even in the context of complex software developments. In parallel, the techniques to design and implement static analysis tools have improved significantly, and much effort is being put into engineering the tools. This workshop is intended to promote discussions and exchange experience between specialists in all areas of program analysis design and implementation and static analysis tool users.

Previous workshops have been held in Perpignan, France (2010), Venice, Italy (2011), Deauville, France (2012), and Seattle, WA, USA (2013).

TAPAS 2014 will be co-located with SAS 2014.

Scope

The technical program of TAPAS 2014 will consist of invited lectures together with presentations based on submitted abstracts.

Submitted presentation abstracts can cover any aspect of program analysis tools including, but not limited to the following:

• design and implementation of static analysis tools (including practical techniques used for obtaining precision and performance)
• components of static analysis tools (front-ends, abstract domains, etc.)
• integration of static analyzers (in proof assistants, test generation tools, IDEs, etc.)
• reusable software infrastructure (analysis algorithms and frameworks)
• experience reports on the use of static analyzers (both research prototypes and industrial tools)

Submission of Presentation Abstracts

All submitted abstracts will be reviewed by the program committee.

Submitted abstracts should be 1-2 pages.

Please submit your abstract as a PDF via EasyChair: https://www.easychair.org/conferences/?conf=tapas2014

See accepted contributions below.

Invited Speakers

• Alexey Loginov, GrammaTech
• David Pichardie, ENS Cachan
• Eric Bodden, Fraunhofer SIT, Technische Universität Darmstadt
• Yannis Smaragdakis, University of Athens
• Werner Dietl, University of Waterloo

See titles and abstracts below.

Dates

• Submission deadline: June 27
• Notification of acceptance: July 11
• Final version due: July 25
• Early registration: On or before July 20, 2014
• Workshop day: September 10, 2014

Venue, Registration, and Accommodation

Please refer to the SAS 2014 website.

Organizers

Anders Møller, Aarhus University (chair)
Ondrej Lhotak, University of Waterloo
Antoine Miné, École Normale Supérieure
Manu Sridharan, Samsung Research America
Hongseok Yang, University of Oxford

Program

9.00 - 9.45 Alexey Loginov: Machine-code analysis and transformation at GrammaTech

In this talk, I will overview GrammaTech's work on machine-code analysis for diverse purposes of reverse engineering, program transformation, and vulnerability detection. I will highlight some challenges and successes in the creation of intermediate representations that aim to reach the depth of information available at the source-code level. The quality of our intermediate representation has allowed us to transform programs for diversification and hardening against attacks, optimization, and intellectual-property protection without modifying program behavior, as validated by extensive test suites.

In addition to variation in the purpose of program analysis, GrammaTech's work on machine-code analysis varies soundness guarantees afforded by different techniques. Not surprisingly, relaxing soundness guarantees can result in improved scalability and precision of analyses. However, unsound analyses require heuristics that balance weakened guarantees against increased scalability and precision. These heuristics themselves often require sophisticated analyses. I will touch on challenges that are unique to performing heuristic analysis.

9.45 - 10.30 Yannis Smaragdakis: Declarative Static Program Analysis

We discuss the benefits of using logic-based declarative languages as a means to specify static program analysis algorithms. The main focus will be on the Doop framework for pointer analysis of Java programs. Doop encodes multiple analysis algorithms for Java declaratively, using Datalog: a logic-based language for defining (recursive) relations. The algorithms are elegantly specified and easy to understand and adapt. With an aggressive optimization methodology, Doop also achieves very high performance--often a factor of 10 faster than other comparable frameworks. With the help of Doop's concise algorithm representation we have explored several new analysis algorithms and developed important insights on existing algorithm variations.

10.30 - 11.00 coffee break

11.00 - 11.30 Sebastian Biallas, Stefan Kowalewski, Stefan Stattelmann and Bastian Schlich: Static Analysis of Industrial Controller Code using Arcade.PLC

11.30 - 12.00 Sven Mattsen, Arne Wichmann and Sibylle Schupp: BDDStab: BDD-based Value Analysis of Binaries

12.00 - 13.30 lunch break

13.30 - 14.15 Werner Dietl: The Checker Framework: pluggable static analysis for Java

Developing a static analysis tool requires a large investment in infrastructure. The Checker Framework provides a feature-rich framework to develop static analysis tools, especially type systems, for Java source code. Researchers can use the Checker Framework to implement novel source code analyses that can be used in case studies of millions of lines of existing Java code. Software developers can use the Checker Framework to enforce fine-grained, domain-specific properties while using a mainstream programming language. In this talk I will highlight a few of the Checker Framework features, discuss its use for Android security and crowd-sourced verification using games, and show how to implement a simple type system from scratch. The Checker Framework is open-source and available from http://checkerframework.org/.

14.15 - 15.00 David Pichardie: Formal Verification of a C Static Analyzer

We report on the design and soundness proof, using the Coq proof assistant, of Verasco, a static analyzer based on abstract interpretation for most of the ISO C 1999 language (excluding recursion and dynamic allocation), which establishes the absence of run-time errors in the analyzed programs. Verasco enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. Verasco integrates with the CompCert C formally-verified compiler so that not only the soundness of the analysis results is guaranteed with mathematical certitude, but also the fact that these guarantees carry over to the compiled executable code.

15.00 - 15.30 coffee break

15.30 - 16.15 Eric Bodden: What's that app doing with my data? - Challenges and solutions to practical taint analysis

Smartphone applications are ubiquitous, but often they are badly programmed or outright malicious. How can we tell apart the good from the bad and the ugly? In this talk I will highlight two challenges to the automated static taint analysis of Android applications. The first challenge is to identify suitable sources and sinks, i.e., the Android API methods that applications can use or misuse to retrieve or send out private data. I will explain the internals of SuSi, a tool that we recently developed for automatically identifying such sources and sinks. The second challenge is to track data flows with high precision and efficiency, while at the same time not only being able to report the kind of flow but even its trace through the app's code. I will explain how our taint tracker FlowDroid deals with this challenges, and what tricks it uses to keep the analysis efficient. FlowDroid, by now, is heavily used by several research groups around the world. Last but not least, also we have not solved all problems in this area. Hence I will explain a few open challenges as well.

16.30 - 18.00 NSAD