The Fifth Workshop on Tools for Automatic Program Analysis
September 10, 2014
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.
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)
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:
See accepted contributions below.
See titles and abstracts below
- 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
Please refer to the SAS 2014 website.
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
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
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
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
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