Previous terms: F12 S12 F11 S11 W11 F10 S10 F08 S08 W08 F07 W07 F06 S06 W06
|Date||Speaker||Title (click for abstract)||Location|
|Mon. Jan. 14, 2013 at 1:30 pm||Omer Tripp||Detecting and Preventing Web Application Security Vulnerabilities via Program Analysis||DC 1304|
|Thu. Jan. 24, 2013 at 2:30 pm||Nomair A. Naeem||Typestate-like Analysis of Multiple Interacting Objects||DC 2314|
|Mon. Mar. 11, 2013 at 2:00 pm||Nomair A. Naeem||Practical Extensions to the IFDS Algorithm||DC 2314|
|Thu. Mar. 14, 2013 at 1:30 pm||Mizra Omer Beg||Constraint Programming in Compiler Optimization||DC 2310|
|Tue. Apr. 2, 2013 at 10:00 am||Nomair A. Naeem||Faster Alias Set Analysis Using Summaries||DC 2314|
|Wed. Apr. 3, 2013 at 10:30 am||Omer Tripp||Specializing Concurrency Control via Analysis of Dynamic Data Dependencies||DC 1304|
|Mon. Apr. 8, 2013 at 10:30 am||Greg Steffan||Programming FPGAs with Software via Overlay Processing Engines||DC 2310|
|Fri. Apr. 12, 2013 at 10:00 am||Karim Ali||Averroes: Whole-Program Analysis without the Whole Program||DC 2314|
All are welcome.
Talk announcements are also posted to a public mailing list.
To volunteer to give a talk, contact Ondřej Lhoták. Talks can range from informal to formal, and they can be about any of the following:
The purpose is for us all to see what people are interested in, and motivate discussions.
In the last five years, I have been a leading member of an IBM project with this goal, collaborating with Marco Pistoia, Takaaki Tateishi, Salvatore Guarnieri, Stephen Fink, Manu Sridharan, and Julian Dolby in IBM, and with Patrick and Radhia Cousot in the academia. In this talk, I will present several research challenges that were addressed as part of this ambitious project, as well as solutions developed in response to these challenges.
Specifically, my talk will survey three main areas of research I led under the broad umbrella of web security:
1. Server-side security verification, where we have developed novel slicing and bounded-analysis techniques (PLDI'09), as well as algorithms for demand-driven analysis with incremental scanning capabilities (to appear in FASE'13; joint work with Prof. Patrick Cousot and Dr. Radhia Cousot);
3. Dynamic testing of Web applications, where we have built a rich and unique database of security attacks, and designed learning algorithms atop this database, to enable rapid convergence on a payload that penetrates through the Web site's defenses during testing, if one exists, with high coverage and performance guarantees (under submission).
Beyond these four main topics, I will quickly go through several other related research works that I took part in, including
1. Mining and verification of server-side security defenses (ACM SIGSOFT Distinguished Paper at ISSTA'11; journal version to appear in TOSEM'13);
2. Framework modeling in static security analysis (OOPSLA'11); and
3. Agent-based testing of mobile applications (work in progress).
I will also provide a brief sketch of my main research areas and results in my
PhD work, which concerns code parallelization and synchronization protocols.
Typestate-like Analysis of Multiple Interacting Objects
Nomair A. Naeem
Jan. 24, 2013
This talk will present a static analysis of typestate-like temporal specifications of groups of interacting objects, which are expressed using tracematches. Whereas typesate expresses a temporal specification of one object, a tracematch state may change due to operations on any of a set of related objects bound by the tracematch. We propose a lattice-based operational semantics equivalent to the original tracematch semantics but better suited to static analysis. We define a static analysis that computes precise local points-to sets and tracks the flow of individual objects, thereby enabling strong updates of the tracematch state. The analysis has been proved sound with respect to the semantics. A context-sensitive version of the analysis has been implemented as instances of the IFDS and IDE algorithms. The analysis was evaluated on tracematches used in earlier work and found to be very precise. Remaining imprecisions could be eliminated with more precise modeling of references from the heap and of exceptional control flow.
Practical Extensions to the IFDS Algorithm
Nomair A. Naeem
Mar. 11, 2013
In this talk, I will present four extensions to the Interprocedural Finite Distributive Subset (IFDS) algorithm that make it applicable to a wider class of analysis problems. IFDS is a dynamic programming algorithm that implements context-sensitive flow-sensitive interprocedural dataflow analysis. The first extension constructs the nodes of the supergraph on demand as the analysis requires them, eliminating the need to build a full supergraph before the analysis. The second extension provides the procedure-return flow function with additional information about the program state before the procedure was called. The third extension improves the precision with which phi instructions are modelled when analyzing a program in SSA form. The fourth extension speeds up the algorithm on domains in which some of the dataflow facts subsume each other. These extensions are often necessary when applying the IFDS algorithm to non-separable (i.e. non-bit-vector) problems. We have found them necessary for alias set analysis and multi-object typestate analysis. In this talk, we illustrate and evaluate the extensions on a simpler problem, a variation of variable type analysis.
Constraint Programming in Compiler Optimization
Mizra Omer Beg
Mar. 14, 2013
In this talk I will demonstrate that difficult combinatorial problems which arise in optimizing compilers can be practically solved using constraint programming techniques. Constraint programming is a methodology for solving hard combinatorial problems, where a problem is modeled in terms of variables, values and constraints. In this talk I will present constraint programming solutions for two important compiler optimization problems, namely, spatial and temporal scheduling and instruction selection.I will show that by using constraint programming techniques it is possible to solve these difficult optimization problems efficiently and more precisely than existing heuristic solutions.
Faster Alias Set Analysis Using Summaries
Nomair A. Naeem
Apr. 2, 2013
Alias sets are an increasingly used abstraction in situations which require flow-sensitive tracking of objects through different points in time and the ability to perform strong updates on individual objects. The interprocedural and flow-sensitive nature of these analyses often make them difficult to scale. In this talk, we present two types of method summaries (callee and caller) to improve the performance of an interprocedural flow- and context-sensitive alias set analysis. We present callee method summaries and algorithms to compute them. The computed summaries contain sufficient escape and return value information to selectively replace flow-sensitive analysis of methods without affecting analysis precision. When efficiency is a bigger concern, we also use caller method summaries which provide conservative initial assumptions for pointer and aliasing relations at the start of a method. Using caller summaries in conjunction with callee summaries enables the alias set analysis to flow-sensitively analyze only methods containing points of interest thereby reducing running time. We present results from empirically evaluating the use of these summaries for the alias set analysis. Additionally, we also discuss precision results from a realistic client analysis for verifying temporal safety properties. The results show that although caller summaries theoretically reduce precision, empirically they do not. Furthermore, on average, using callee and caller summaries reduces the running time of the alias set analysis by 27% and 96%, respectively.
Specializing Concurrency Control via Analysis of Dynamic Data Dependencies
Apr. 3, 2013
Software applications are becoming increasingly harder to parallelize. Modern software systems written in imperative languages like Java and C# typically manipulate complex heap data structures, consist of multiple layers of abstraction, and have input- and deployment-specific behaviors that affect their available parallelism.
This creates a significant challenge for parallelizing compilers, whose target transformations are normally conditioned on the assumption that the instructions designated for parallel execution access disjoint memory regions. Establishing this precondition over real-world applications is hard: Often there are dependencies between the candidate code blocks at the concrete level, at least over some of the inputs, and even if disjointness holds universally, it is hard for an automated verifier to formulate a proof to this effect.
These limitations of static dependence analysis in dealing with the complexity of modern programs, as well as their dynamic behavior, have shifted attention to runtime optimistic parallelization techniques, and most notably, software transactional memory (STM). The challenge with this approach is that STM typically incurs high overhead -- due mainly to runtime tracking of memory accesses and conservative conflict detection -- which often obviates the performance gain from parallelization.
In this talk, I shall describe techniques for overcoming the limitations of these general parallelization techniques by specializing the parallelization system per the specific application and workload at hand. Specialization addresses fluctuating parallelism, as evidenced in many applications, and enables optimizing the runtime system with respect to prevalent program behaviors and common input profiles.
Specifically, I will present methods for specializing concurrency control by analyzing dynamic data dependencies, obtained during offline profiling over representative executions of the subject program. I will demonstrate that these methods enable effective specialization over realistic programs and popular parallelization techniques, e.g. by dramatically reducing STM overhead thanks to specialized conflict detection.
Omer Tripp is a final-year PhD student of Prof. Mooly Sagiv at
Tel-Aviv University. In his PhD research, Omer applied techniques from the
area of program analysis to optimize and specialize concurrency control. Omer
is also a researcher at IBM, where he holds a nomination as Master Inventor.
Omer's research at IBM focuses on program analysis for web and mobile security.
Programming FPGAs with Software via Overlay Processing Engines
Apr. 8, 2013
Field-Programmable Gate Arrays (FPGAs) are becoming increasingly common in computing products because they provide very low-risk access to VLSI technology and faster time-to-market compared to fully-fabricated chips. However, the use of FPGAs has faced two increasingly daunting barriers: (i) the relative difficulty of designing hardware, which is typically done at the Register-Transfer-Level (RTL) in hardware description languages by specialized hardware engineers; and (ii) the large computational effort needed by the CAD tools to translate and optimize the RTL design for an FPGA, which can take up to a day for a large design (ie., a very slow turn-around time for design iteration).
In this talk I will describe my group's recent research to address these problems via "overlay processing engines": pre-designed soft structures for FPGAs that are themselves software programmable. The simplest example of an overlay engine is a "soft processor"---i.e., an instruction set processor built using the programmable logic of an FPGA. More advanced engines we have developed include soft vector processors for embedded computing and multithreaded processors for network packet processing. In this talk I will summarize some of our more recent work on a super-fast multithreaded processor, a multithreaded VLIW engine, and work towards building multicores of these engines.
Greg Steffan is an Associate Professor and the Jeffrey Skoll Chair in Software
Engineering, Department of Electrical and Computer Engineering at the
University of Toronto. His research focus is on making multicore processors
and FPGAs easier to program. He completed his doctorate at Carnegie Mellon
University in 2003, after undergraduate and Masters degrees at the University
of Toronto. He is a Siebel Scholar (2002), an IBM CAS Faculty Fellow and
Visiting Scientist, and a senior member of both the IEEE and ACM.
Averroes: Whole-Program Analysis without the Whole Program
Apr. 12, 2013
Call graph construction is costly and impractical because it analyzes the whole program. The separate compilation assumption (SCA) makes it possible to generate sound and reasonably precise call graphs without analyzing libraries. We investigate whether the SCA can be encoded in Java bytecode. We evaluate Averroes, a tool that generates a placeholder library that overapproximates the possible behaviour of an original library. The placeholder library can be constructed quickly and is typically smaller in size. Any existing whole-program framework can use the placeholder library to efficiently construct sound and precise application call graphs. Typical efficiency improvements are a factor of 4x to 12x in time, and 8x to 13x in memory. In addition, Averroes makes it easier to handle reflection soundly. The call graphs built with Averroes are as precise and sound as those built with Cgc, which implements the SCA explicitly in Doop.