|
|
||
Past Research Accomplishments
Capsule SummariesDuring my 45-year career in Computer Science, the overriding goal of my research has been to find new ways to help programmers create correct, reliable, and secure software. To address these issues, I developed a number of new methods to manipulate programs and analyze their properties. Often these have taken the form of frameworks that apply to general classes of problems, e.g.,
My research interests have spanned program-development environments, software engineering, dataflow analysis, and more recently, computer security, software verification, and program synthesis, with some excursions into other subjects, as well. The key achievements can be summarized as follows:
Interactive Program-Development Environments
The Cornell Program Synthesizer [TR81], which Tim Teitelbaum and I started working on in 1978, was the first example of an interactive program-development environment with integrated, screen-oriented facilities for a strongly-typed, block-structured, imperative programming language. It had a tightly integrated combination of facilities for programmers to create, edit, execute, monitor, single-step, and debug their PL/C programs. In other words, by 1979, we had created the first version of an interactive programming environment similar to modern tools, such as Microsoft Visual Studio and Eclipse. At the time that it was created (1978-79), the Cornell Program Synthesizer was a radically new kind of programming tool. Along with the Mentor system of Donzeau-Gouge, Kahn, Huet, and Lang [DGKHL80], it showed that the kind of direct-manipulation programming tools that had been pioneered in the SmallTalk and InterLisp systems could be created for a mainstream programming language (i.e., one that was strongly-typed, block-structured, and had imperative programming constructs). The Cornell Program Synthesizer was used successfully in introductory programming classes by about 20,000 students over a five-year period at Cornell, Rutgers, Princeton, UCLA, and several other universities. The Cornell Program Synthesizer was distributed to researchers at about 110 universities, research institutes, and industry laboratories. Through lectures that were given about the system and copies that were distributed, it is possible to trace its direct influence on several commercial products, including DEC's Language Sensitive Editor, Rational's Ada programming environment, and Symantec's LightspeedC and LightspeedPascal programming environments. It is more difficult to connect the dots to the similar products that hundreds of thousands or millions of people use on a daily basis today; however, together with the initial paper about the system [TR81], the Cornell Program Synthesizer was very influential: as a model for programming tools of the future, it helped to spark widespread interest in the question of how to create better tools for developing, analyzing, testing, and debugging programs. My Ph.D. dissertation [R84], which was honored with the 1983 ACM Doctoral Dissertation Award, investigated the problem of automating the creation of programming tools similar to the Cornell Program Synthesizer, but for languages other than PL/I. The goal of the research was to create an editor-generator tool to enable editors for different languages to be created automatically from a language description. In the solution I proposed, language descriptions are specified by giving
As part of my Ph.D. research, I developed a prototype implementation of an editor-generating system that made use of the ideas described above. I spent 1982-85 as a post-doc at Cornell (in residence during 1982-83 at INRIA, the national institute for computer science in France) collaborating with Tim Teitelbaum on the design and implementation of the Synthesizer Generator, a full-scale version of such a system [RT84, RT87, RT88a]. The Synthesizer Generator creates a language-specific editor from an input specification that defines a language's syntax, display format, transformation rules for restructuring "documents" written in the language, and attribution rules that codify context-sensitive relationships between document elements. From this specification, the Synthesizer Generator creates a specialized editor for manipulating documents according to these rules. The Synthesizer Generator has proven to be of great utility in a wide range of applications, including program editors, text-preparation systems, and tools that verify the correctness of proofs (for several different kinds of mathematical and programming logics [RA84, G88, GMP90]). In 2010, our 1984 paper about the Synthesizer Generator [RT84] received an ACM SIGSOFT Retrospective Impact Paper Award. Beginning in August 1985, the Synthesizer Generator was made available to universities and industrial research organizations. Since distribution began it has been licensed to about 330 sites in 23 countries. Two books describing the system, which Teitelbaum and I co-authored, were published by Springer-Verlag in 1988 [RT88a, RT88b]. Also in 1988, Teitelbaum and I founded a company (GrammaTech, Inc.) to commercialize the Synthesizer Generator technology. GrammaTech subsequently created two products for the Ada programming language based on the Synthesizer Generator, Ada-ASSURED and Ada-Utilities, and, since the mid-90's, these have been used in the development of almost every major Department of Defense system written in Ada.
Software EngineeringStarting in 1986, I carried out a great deal of work exploring how program slicing (an operation originally proposed in 1979 by the late Mark Weiser) can serve as the basis for semantics-based program-manipulation operations. The slice of a program with respect to a set of program elements S is a projection of the program that includes only program elements that might affect (either directly or transitively) the values of the variables used at members of S. Slicing allows one to find semantically meaningful decompositions of programs, where the decompositions consist of elements that are not textually contiguous. Program slicing is a fundamental operation that can aid in solving many software-engineering problems [HR92]. For instance, it has applications in program understanding, maintenance, debugging, testing, differencing [HR91], specialization [RT96], reuse, and merging of program variants [HPR89]. The projects that I carried out with my students and co-workers were aimed at
The conference paper on interprocedural slicing that Susan Horwitz, David Binkley, and I wrote [HRB88] was selected for inclusion in a special SIGPLAN collection of the 50 most influential papers from the SIGPLAN Conference on Programming Language Design and Implementation from 1979 to 1999:
A journal version of [HRB88] appeared as [HRB90]. (Of all my papers, this is the most highly-cited; e.g., see Google Scholar and CiteseerX.) A retrospective on [HRB88] was published as
In 2011, our 1994 paper "Speeding up slicing" [RHSR94] received an ACM SIGSOFT Retrospective Impact Paper Award. In more recent work, my students, colleagues, and I have developed even better methods for program analysis and slicing based on a formalism called weighted pushdown systems. In collaboration with Genevieve Rosay and Susan Horwitz, I built a system, called the Wisconsin Program-Slicing Tool, that implemented slicing of ANSI C programs. Although the Wisconsin Program-Slicing Tool was distributed from 1996-2000 for not-for-profit research purposes under license from the University of Wisconsin, it is no longer being distributed. However, there is a commercial tool available, named CodeSurfer, that is derived from the Wisconsin implementation and is available from GrammaTech, Inc., which licensed the technology from the Wisconsin Alumni Research Foundation (a not-for-profit foundation that uses royalty income from the technologies it licenses to support research at the University of Wisconsin). GrammaTech has improved on the Wisconsin implementation considerably (both in terms of speed and space efficiency), and extended it to support C++. GrammaTech also offers CodeSurfer to academic researchers on very favorable terms. In 2007, Tavis Ormandy of Gentoo Linux said the following about CodeSurfer: "Our team is responsible for investigating and verifying security problems in any of the 10,000+ open source programs we distribute. CodeSurfer has made a dramatic impact on the time it takes us to isolate and understand security flaws, allowing us to traverse complex and unfamiliar codebases easily and trace problems to their source."A group at SAIC/NASA had this to say about CodeSurfer: "Our group analyzes many mission-critical software projects to reduce defects and ensure that the software meets requirements. We conducted a formal study to see if CodeSurfer could improve our software inspections. We found that CodeSurfer reduced inspection time by an average of 30%. In addition, when using CodeSurfer the number of defects found more than doubled." Slicing was also used in many commercial tools that were developed to address such code-renovation issues as the Year 2000 Problem ("Y2K bug") and conversion of financial software to support adoption of the Euro. One example is IBM's Rational Transformation Workbench. (A list of more than 20 such tools can be found here.)
My student Mike Siff and I investigated techniques for converting C programs to C++ programs that take advantage of the improved features of C++, such as templates and classes. For instance, in [SR96] we considered the problem of software generalization: Given a program component C, create a parameterized program component C' such that C' is usable in a wider variety of syntactic contexts than C. Furthermore, C' should be a semantically meaningful generalization of C; namely, there must exist an instantiation of C' that is equivalent in functionality to C. We gave an algorithm that generalizes C functions via type inference: the original functions operate on specific data types; the result of generalization is a collection of C++ function templates that operate on parameterized types. We also described a general technique for identifying modules in legacy code [SR99]. The method is based on concept analysis—a branch of lattice theory that can be used to identify similarities among a set of objects based on their attributes. We showed how concept analysis can identify potential modules using both "positive" and "negative" information, and presented an algorithmic framework to construct a lattice of concepts from a program, where each concept represents a potential module. The development of better techniques for software renovation was the subject of Mike Siff's Ph.D. dissertation [S98].
In 1996, I was asked by the Defense Advanced Research Projects Agency (DARPA) to plan a project aimed at reducing the impact of the Year 2000 problem on the Department of Defense. DARPA was particularly interested in whether there were "any techniques in the research community that could be applied to the Y2K problem and have impact beyond present commercial Y2K products and services." I spent a semester as a kind of talent scout for DARPA to see what ideas might be worth pursuing. The most exciting of the ideas that turned up concerned a method for using path profiling as a heuristic to locate some of the sites in a program where there are problematic date manipulations [RBDL97] (and more generally as an aid for testing and debugging). A path profiler instruments a program so that the number of times each different loop-free path executes is accumulated during an execution run. With such an instrumented program, each run of the program generates a path spectrum for the execution—a distribution of the paths that were executed during that run. A path spectrum is a finite, easily obtainable characterization of a program's execution on a dataset, and provides a behavior signature for a run of the program. Our techniques are based on the idea of comparing path spectra from different runs of the program. When different runs produce different spectra, the spectral differences can be used to identify paths in the program along which control diverges in the two runs. By choosing input datasets to hold all factors constant except one, the divergence can be attributed to this factor. The point of divergence itself may not be the cause of the underlying problem, but provides a starting place for a programmer to begin his exploration. One application of this technique is in the "Year 2000 Problem" (i.e., the problem of fixing computer systems that use only 2-digit year fields in date-valued data). In this context, path-spectrum comparison provides a heuristic for identifying paths in a program that are good candidates for being date-dependent computations.
A few years later, we found out that essentially the same idea had been discovered earlier by J. Collofello and L. Cousin [CC87], as well as by N. Wilde (who has done extensive research on the subject, and uses the term "software reconnaissance", e.g., see [W94, WC96]).
Dataflow AnalysisInterprocedural Dataflow Analysis and Context-Free-Language ReachabilityWork that I carried out with Susan Horwitz, Mooly Sagiv, and David Melski established some interesting connections between the work on interprocedural program slicing and a number of other program-analysis problems, such as classical interprocedural dataflow analysis. In particular, we showed that a large class of program-analysis problems can be solved by transforming them into instances of a special kind of graph-reachability problem, called context-free-language reachability (CFL-reachability) [RHS95, HRS95, R95b, R96, MR98, R98, R00]. CFL-reachability is the variant of reachability in which a path from node s to node t only counts as a valid s-t connection if the path's labels form a word in a given context-free language. The notion of CFL-reachability was originated by Mihalis Yannakakis, who developed it in the context of graph-theoretic methods in database theory. Context-free-language reachability problems can be solved in polynomial time by algorithms similar to the ones we originally developed for interprocedural slicing [HRB90, RHSR94]. David Melski and I studied the relationship [MR98] between CFL-reachability and the program-analysis formalism of set constraints, which was introduced by John Reynolds and subsequently studied by Alex Aiken and Nevin Heintze. The PowerPoint presentation prepared for the tutorial that I gave on this material at PLDI '00 can be found here. In more recent work, my students, colleagues, and I have developed even better methods for interprocedural dataflow analysis based on a formalism called weighted pushdown systems. In addition to the CFL-reachability-based slicing algorithms that are used in CodeSurfer, the work on program analysis via CFL-reachability had direct impact on many systems for software model checking and bug detection: a CFL-reachability solver is one of the key analysis components used in most such systems. Among them is the well-known SLAM tool from Microsoft, which checks C programs against temporal safety properties to find defects in Windows device drivers—thereby addressing one of Windows' main weak points. In particular, as described in [BR01], one of the key algorithms used in SLAM is based on the interprocedural dataflow-analysis algorithm given in [RHS95]. Due to the importance of the problem that it addressed, the SLAM work even got on Bill Gates's radar screen. For instance, in a keynote address at the Windows Hardware Engineering Conference in 2002, Gates touted the work on SLAM as follows: "… software verification … has been the Holy Grail of Computer Science for many decades, but now in some very key areas, for example, driver verification, we're building tools that can do actual proof about the software and how it works in order to guarantee the reliability." (See also Gates's address at OOPSLA 2002.) Thus, as one of the key technologies in a tool that has helped to make Windows much more stable in recent years, CFL-reachability has had a significant impact on the computing experience of hundreds of millions of people worldwide.
The technique for static program analysis using 3-valued logic that Mooly Sagiv, Reinhard Wilhelm, and I developed [SRW02, RSW04] addresses the problem of analyzing programs that use dynamic allocation and freeing of storage cells and destructive updating of structure fields—features found in all modern programming languages, including C, C++, and Java. In such programs, data structures can grow and shrink dynamically, with no fixed upper bound on their size or number. In the case of thread-based languages, such as Java, the number of threads can also grow and shrink dynamically. We developed a way to create finite-sized descriptors of memory configurations that (i) abstract away certain details, but (ii) retain enough key information so that the analysis can identify interesting properties that hold. We used these ideas to create a framework for program analysis that is capable of expressing rich properties of memory configurations, and confirming such behavioral properties as
The work was originally motivated by the problem of shape analysis for programs written in languages that permit destructive updating of dynamically allocated storage. The aim of shape analysis is to discover information (in a conservative way) about the possible "shapes" of the dynamically allocated data structures to which a program's pointer variables can point. As we investigated this problem more deeply, we discovered methods that allowed us to deal with properties of memory configurations other than just pure shape properties. For instance, recent work has concerned numeric properties [GDDRS04]. The key aspect of our approach is the way in which it makes use of 2-valued and 3-valued logic: 2-valued and 3-valued logical structures—i.e., collections of relations—are used to represent concrete and abstract stores, respectively; individuals represent entities such as memory cells, threads, locks, etc.; unary and binary relations encode the contents of variables, pointer-valued structure fields, and other aspects of memory states; and first-order formulas with transitive closure are used to specify properties such as sharing, cyclicity, reachability, etc. Formulas are also used to specify how the store is affected by the execution of the different kinds of statements in the programming language. The analysis framework can be instantiated in different ways by varying the relation symbols of the logic, and, in particular, by varying which of the unary relations control how nodes are folded together. The specified set of relations determines the set of properties that will be tracked, and consequently what properties of stores can be discovered to hold at different points in the program by the corresponding instance of the analysis. As a methodology for verifying properties of programs, the advantages of the 3-valued-logic approach are:
A prototype implementation that implements this approach has been created, called TVLA (Three-Valued-Logic Analyzer). In addition to [SRW02, RSW04], some of the other key papers about this work include those on interprocedural shape analysis [JLRS04, JLRS08], numeric properties together with shape properties [GDDRS04], applications to program verification [LRSW00, LRS06, LRS07, ARRSY07], the use of ideas from incremental computing and databases to construct abstract transformers [RSL03, RSL10, EGR10], and the use of machine learning to identify appropriate abstractions [LRS05]. The Ph.D. dissertations of Alexey Loginov [L06] and Denis Gopan [G07] developed improved techniques for static analysis based on 3-valued logic.
The framework for interprocedural dataflow analysis that Somesh Jha, Stefan Schwoon, and I developed, based on weighted pushdown systems [RSJM05], supports a strictly richer set of queries than previous approaches to interprocedural dataflow-analysis (a problem that has a 35-year history). In general, the approach can be applied to any distributive dataflow-analysis problem for which the domain of transfer functions has no infinite descending chains (including problems that cannot be expressed as bit-vector problems, such as linear constant propagation [SRH96] and affine-relation analysis [MOS04]). Safe solutions are also obtained for problems that are monotonic but not distributive. The benefits of the approach can be summarized as follows:
Weighted pushdown systems are also a useful formalism in a completely separate application domain, namely, access control of shared computing resources in distributed systems [JR02, SJRS03, JR04, JSWR06, WJRSS06]. The algorithms described in [RSJ03, RSJM05], along with the improvements described in [LRB05, LR06, LKRT07, LR08b], have been implemented in two libraries for use in creating program-analysis tools [KRML04, KLR07]. These libraries have been used to create prototype implementations of context-sensitive interprocedural dataflow analyses for uninitialized variables, live variables, linear constant propagation, and the detection of affine relationships, as well as many other problems. In our work on static analysis of stripped executables, we devised methods that—without relying on symbol-table or debugging information—recover intermediate representations that are similar to those that the intermediate phases of a compiler create for a program written in a high-level language. The goal is to provide a platform that an analyst can use to understand the workings of COTS components, plugins, mobile code, and DLLs, as well as memory snapshots of worms and virus-infected code. Starting from a stripped executable, our algorithms identify variables, data objects, and types, and track how they are manipulated by the executable. This information provides answers to such questions as "what could this dereference operation access?", "what function could be called at this indirect call site?", etc. Our initial work concerned x86 executables. In 2003, my student Gogul Balakrishnan and I developed a static-analysis algorithm for x86 machine code that is able to track the flow of values through memory [BR04]. We incorporated this algorithm, along with algorithms to identify variables, data objects, and types, in CodeSurfer/x86 [BGRT05]—the first program-slicing tool for machine code that can help with understanding dependences across memory updates and memory accesses. Later, we extended CodeSurfer/x86 to create the first automatic program-verification tool for stripped executables: it allows one to check that a stripped executable conforms to an API-usage rule (specified as a finite-state machine) [BRKLLMGYCT05, BR08]. More recently, our work on the TSL system has allowed us to create similar systems for other instruction sets automatically, starting from a specification of the concrete semantics of a machine-code instruction set. Static analysis of machine code was the subject of Gogul Balakrishnan's Ph.D. dissertation [B07]. See also our ACM TOPLAS paper about the work [BR10]. (The 2004 paper about the work [BR04] received the ETAPS Best-Paper Award for 2004 from the European Association for Programming Languages and Systems (EAPLS).)
In 2008, my student Junghee Lim and I created the TSL system [LR08a, LR12], a meta-tool to help in the creation of tools for analyzing machine code. (TSL stands for Transformer Specification Language.) From a single specification of the concrete semantics of a machine-code instruction set, TSL automatically generates correct-by-construction implementations of the state-transformation functions needed in state-space-exploration tools that use static analysis, dynamic analysis, symbolic analysis, or any combination of the three [LR08a, LLR09a, LLR10, TLLBDEAR10]. The TSL language is a strongly typed, first-order functional language with a datatype-definition mechanism for defining recursive datatypes, plus deconstruction by means of pattern matching. Writing a TSL specification for an instruction set is similar to writing an interpreter in first-order ML. For instance, the specification of an instruction set's concrete semantics is written as a TSL function
state interpInstr(instruction I, state S) {...};
where instruction and state are user-defined
datatypes that represent the instructions and the semantic states,
respectively.
TSL's meta-language provides a fixed set of base-types; a fixed set of arithmetic, bitwise, relational, and logical operators; and a facility for defining map-types. The meanings of the meta-language constructs can be redefined by supplying alternative interpretations of them. When semantic reinterpretation is performed in this way—namely, on the operations of the meta-language—it is independent of any given instruction set. Consequently, once a reinterpretation has been defined that reinterprets TSL in a manner appropriate for some state-space-exploration method, the same reinterpretation can be applied to each instruction set whose semantics has been specified in TSL. The reinterpretation mechanism causes TSL to act as a "Yacc-like" tool for automatically generating correct-by-construction implementations of the state-transformation functions needed in state-space-exploration tools. Moreover, because all components are generated from a single specification of the concrete semantics of an instruction set, the generated implementations are guaranteed to be mutually consistent (and also to be consistent with an instruction-set emulator that is generated from the same specification of the concrete semantics). TSL was the subject of Junghee Lim's Ph.D. dissertation [L11]. (The 2008 paper about TSL [LR08a] received the ETAPS Best-Paper Award for 2008 from the European Association for Programming Languages and Systems (EAPLS).)
Since 2002, I have been interested in symbolic methods for abstract interpretation. The work aims to bridge the gap between (i) the use of logic for specifying program semantics and performing program analysis, and (ii) abstract interpretation [RSY04, YRS04, TR12a, TR12b, TER12, ELSAR13, TLLR13]. In [RSY04], Mooly Sagiv, Greta Yorsh, and I gave the first method that makes such a connection: we showed that, for a broad class of situations, given a formula φ in some logic L, it is possible to find the best value a in a given abstract domain Abs that over-approximates the meaning of φ (i.e., [[φ]] ⊆ γ(a)). We call this problem symbolic abstraction. If you think of logic L as being a rich language for expressing meanings, and abstract domain Abs as corresponding to a logic fragment L' that is less expressive than L, then symbolic abstraction addresses a fundamental approximation problem: Given φ ∈ L, find the strongest consequence of φ that is expressible in logic fragment L'. From 2011 to 2016, my student Aditya Thakur and I pursued the insight that generalized versions of an old, and not widely used, method for validity checking of propositional-logic formulas, called Stålmarck's method, hold great promise for symbolic abstraction. The symbolic methods for abstract interpretation that we have subsequently developed based on this insight [TR12a, TR12b, TER12, TLLR13] offer much promise for building more powerful program-analysis tools. These methods (i) allow more precise implementations of abstract-interpretation primitives to be created, and (ii) drastically reduce the time taken to implement such primitives because correctness is ensured by construction. In particular, they provide a way to create correct-by-construction abstract interpreters that also attain the fundamental limits on precision that abstract-interpretation theory establishes. For instance, in [TLLR13], we described a systematic method for implementing an abstract interpreter that solves the following problem: Given program P, and an abstract domain A, find the most-precise inductive A-invariant for P. Moreover, our generalized-Stålmarck methods are "dual-use": In addition to providing methods for building improved abstract-interpretation tools, they also provide methods for building improved logic solvers that use abstract interpretation to speed up the search that a solver carries out.In particular, we showed how Stålmarck's method is an instantiation of a generic framework parameterized by an abstract domain over Booleans; consequently, different instantiations of the framework lead to new decision procedures for propositional logic [TR12b]. Moreover, this abstraction-based view allows us to lift Stålmarck's method from propositional logic to richer logics: to obtain a method for richer logics, instantiate the parameterized version of Stålmarck's method with richer abstract domains [TR12a]. We call such a decision-procedure design, which is parameterized by an abstract domain, a Satisfiability Modulo Abstraction (SMA) solver [RT14]. Recently, we created an SMA solver for separation logic [TBR14]. Separation logic (SL) is an expressive logic for reasoning about heap structures in programs, and provides a mechanism for concisely describing program states by explicitly localizing facts that hold in separate regions of the heap. SL is undecidable in general, but by using an abstract domain of shapes [SRW02] we were able to design a semi-decision procedure for SL. The design of algorithms for symbolic abstraction and their application was the topic of Aditya Thakur's Ph.D. dissertation [T14].
Recently, Esparza et al. generalized Newton's method—the classical numerical-analysis algorithm for finding roots of real-valued functions—to a method for finding fixed-points of systems of equations over semirings. Their method provides a new way to solve interprocedural dataflow-analysis problems. As in its real-valued counterpart, each iteration of their method solves a simpler ``linearized'' problem. However, there is an important difference between the dataflow-analysis and numerical-analysis contexts: when Newton's method is used on numerical-analysis problems, multiplicative commutativity is relied on to rearrange expressions of the form ``a * X * b'' into ``X * a * b.'' Equations of the form ``X = X * a * b'' correspond to path problems described by regular languages. In contrast, when Newton's method is used for interprocedural dataflow analysis, the ``multiplication'' operation involves function composition, and hence is non-commutative: ``X = a * X * b'' cannot be rearranged into ``X = X * a * b,'' and thus the equations correspond to path problems described by linear context-free languages (LCFLs). What we contributed in [RTP17, RTP16] is a way to convert each LCFL problem into a regular-language problem. Given that the language {aibi} is the canonical example of an LCFL that is not regular, this transformation sounds impossible. The secret is that we require the semiring to support a few additional operations (what we call ``transpose,'' ``tensor product,'' and ``detensor''). Moreover, one has such operations for the so-called ``predicate-abstraction problems'' (an important family of dataflow-analysis problems used in essentially all modern-day software model checkers). In predicate-abstraction problems,
(a1t tensor b1) * (a2t tensor b2) = (a1t * a2t) tensor (b1 * b2)
= (a2 * a1)t tensor (b1 * b2)
^ ^ ^ ^
| | | |
| +-------------+ |
+-----------------------+
which produces the kind of mirrored symmetry that we need to properly
track the values that arise in the X system, which have such symmetric
correlations. (More precisely, the detensor operation performs
detensor(at tensor b) = a * b,so that detensor((a2 * a1)t tensor (b1 * b2)) = a2 * a1 * b1 * b2,which has the mirrored symmetry found in the values of derivation trees in the X system.) The Z system's paths encode all and only the derivation trees of the X system. To use this idea to solve an LCFL path problem precisely, there is one further requirement: the ``detensor'' operation must distribute over the tensored-sum operation. This property causes the detensor of the sum-over-all-Z-paths to equal the desired sum-over-all-X-tree-valuations. It turns out that such a distributive detensor operation exists for Kronecker products of Boolean matrices, and thus all the pieces fit together for the predicate-abstraction problems. In addition to the use in Newtonian Program Analysis, we know of two other applications of the rearrangement trick: It was originally used in LTKR08 in a method for context-bounded analysis of concurrent programs; although we used a different method in our work on abstract error projection LKRT07, the rearrangement trick could have been used, and would have improved the result. Zak Kincaid, Jason Breck, John Cyphert, and I have continued this line of research, and developed a number of additional techniques that have been incorporated in a system called ICRA (Interprocedural Compositional Recurrence Analysis), which finds invariants in numeric programs [KBFBR17, KCBR18, KBCR19, CBKR19, BCKR20, KRC21]. That work introduces versions of ``transpose,'' ``tensor product,'' and ``detensor'' for use with logical formulas.
Program SynthesisProgram synthesis refers to the task of finding a program within a given search space that meets a given behavioral specification (typically a logical formula or a set of input-output examples). The general problem is as follows: Given a specification S that relates input values and output values, create a program P that satisfies S—i.e., for all inputs x, the input/output pair (x, P(x)) satisfies S.The benefit of creating software via a synthesis tool is that when the tool produces a program that satisfies S, the program is correct by construction. In our work, we are developing a new synthesis framework, called ``semantics-guided synthesis'' (SemGuS) that attempts to be both language-agnostic and solver-agnostic. The goal of SemGuS is to provide a general, logical framework that expresses the core computational problem of program synthesis, without being tied to a specific solution or implementation. What the SemGuS work brings to the table is the idea of parameterizing the core synthesis algorithm with the semantics of the primitives out of which the target program is to be constructed—hence the name ``semantics-guided synthesis.'' In addition to a syntactic search space and a behavioral specification, SemGuS also allows the user to define the semantics of constructs in the grammar in terms of a set of inference rules. The SemGuS framework is described in [KHDR21, DHKR21], and the SemGuS page is here: semgus.org. SemGuS is another nice illustration of the benefit of developing a solution in the form of a framework: quoting Richard Hamming, it allows the work to address "all of next year's problems, not just the one [currently] in front of [your] face" [H86, p. 7]. Along the way, we obtained new results on how to show that a program-synthesis problem is ``unrealizable'' (i.e., the problem has no solution). While many program synthesizers are good at finding a solution when one exists, they typically fail, or do not terminate, when the given synthesis problem is unrealizable. The lack of knowledge about this problem was an important lacuna in the field: the key to an efficient synthesis algorithm is pruning of the search space; in particular, when synthesis subproblems are unrealizable, one wants that part of the search space to be pruned so that the synthesizer will never again look for a solution there—because none is to be found. Our work has started to fill this gap by introducing multiple approaches for proving that synthesis problems are unrealizable [HBCDR19, HCDR21b]. We also developed techniques for synthesizing programs that meet a user-specified asymptotic-complexity bound [HCDR21a].
Model Checking Concurrent ProgramsIn context-bounded analysis, a program's behavior is explored for a fixed number of context switches; however, running threads are allowed to perform an a priori unbounded amount of work between context switches. Context-bounded analysis was introduced by Shaz Qadeer and Jakob Rehof; however, their algorithm had two drawbacks: (i) it was limited to Boolean abstract domains (i.e., predicate-abstraction domains), and (ii) it performed certain enumerations of reachable configurations during the process of state-space exploration. In 2008, Akash Lal, Tayssir Touili, Nicholas Kidd, and I showed how symbolic methods could be employed in context-bounded analysis. In particular, we gave transducer-based techniques that permit the explicit-enumeration step of the Qadeer-Rehof algorithm to be avoided [LTKR08]. Akash Lal and I showed how any context-bounded-analysis problem can be tranformed into an equivalent sequential problem; after applying the transformation, any existing tool for sequential analysis can then be applied [LR08c, LR09]. When we compared the performance of the latter analysis technique against a state-of-the-art tool for verifying concurrent device drivers (Daniel Kroening's DDVerify, using SMV as its analysis engine), we found that the median improvement obtained was a 30-fold speedup! (See Figure 7.9 on page 205 of [L09].) Context-bounded analysis was the subject of Akash Lal's Ph.D. dissertation [L09]. For this work, Akash was a co-recipient of the 2009 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award. Akash was also named to MIT Technology Review's 2011 India TR-35 list. In 2023, Akash and I, along with M. Musuvathi, S. Qadeer, and J. Rehof, received the 2023 CAV Award for the ``introduction of context-bounded analysis and its application to systematic testing of concurrent programs.''
Our work on detecting atomicity violations focused on the problem of detecting data races that may involve multiple data locations. Problems can arise when a program is supposed to maintain an invariant over multiple data locations, but accesses/updates are not protected correctly by locks. The tool that we built analyzes Java programs. Originally, the analysis engine in the tool employed a semi-decision procedure; however, after introducing two problem transformations that were motivated by the desire to reduce the imprecision caused by the abstractions that the tool applies [KLR08, KRDV09], we discovered that for the model of concurrent programs we were working with—which permits (i) reentrant locks, (ii) an unbounded number of context switches, and (iii) an unbounded number of lock acquisitions—the problem is decidable [KLTR09]. (The couplings between different processes are sufficiently weak that the undecidability of checking emptiness of the intersection of two context-free languages does not come into play.) When we compared the performance of the decision procedure against the semi-decision procedure, we found that the decision procedure was 34 times faster overall (i.e., comparing the sum of the running times on all queries, with a 300-second timeout). Moreover, with the 300-second timeout threshold, for each query where the semi-decision procedure timed out (roughly 49% of the queries), the decison procedure succeeded within the allotted time. Detection of atomicity violations was the subject of Nicholas Kidd's Ph.D. dissertation [K09].
Policy Weaving
System security is a cross-cutting issue. Unfortunately, it is hard to devise a formalism that allows system-wide policies to be both (i) easily understood and (ii) easily implemented and maintained. In particular, when the elements of security policies are expressed directly in the code—e.g., via calls on security primitives, as in Decentralized Information Flow Control (DIFC) systems, such as Asbestos, HiStar, and Flume, or in capability-based systems, such as Capsicum—the policy implementation is spread throughout the codebase of an application. With such a structure, it is difficult to understand what overall policy the application actually implements, which complicates documenting the policy, debugging the policy, and updating the policy as the codebase evolves in response to changes in requirements and the threat landscape. In contrast, the focus of our work is on a declarative approach to system security. In our approach, a policy specification is a first-class notion—e.g., the policy specification for a given application is a single document, so that all elements of the policy are gathered together in one place, rather than scattered throughout the codebase. A security policy is still implemented in terms of a collection of code snippets to invoke policy-enforcement primitives at different points in the program. However, users are freed from the task of introducing such snippets manually. The goal of our work is to create tools to support policy weaving, which will handle the job of rewriting the program to place code at appropriate locations so that suitable security primitives are invoked at appropriate moments to enforce the policy. A policy-weaving tool takes as input (i) a program P, and (ii) a policy R (written in some suitable policy-specification language), and rewrites P to enforce R. A policy-weaving tool supports a declarative approach to security. The policy R can be stated as a single, easily-understood document, and it is the obligation of the policy-weaving tool to find a way to place code for invoking enforcement primitives so that all executions of P satisfy R. We also work on meta-tools to support policy weaving. In particular, one of our goals is to create a policy-weaver generator. Such a tool takes as input specifications of
Our vision is similar to aspect-oriented programming (in that a cross-cutting issue is specified separately and then automatically woven into the fabric of the implementation). However, the approach that we envision goes beyond aspect-oriented programming in an important way: whereas conventional aspect-oriented programming systems use syntactically-oriented mechanisms and allow aspect code to be placed in a rather limited set of locations, our approach is based on programming-language and policy semantics to identify automatically the program locations where policy-enforcement primitives need to be placed. Our approach also goes beyond simple finite-state reference monitors: policies have visibility into such entities as processes, principals, and communication channels. A key challenge is to design a policy weaver that can reason about the potentially-unbounded set of states that a program may reach, and to choose system primitives and parameters from a potentially unbounded number of options to keep the program from reaching states that constitute a violation of the policy provided by the programmer. Our approach to designing a weaver generator is based on the theory of two-player safety games. Such a game is played by two players, called the Attacker and the Defender, on a graph in which each node is labeled as an Attacker node or a Defender node. The state of the game is a node of the graph. The goal of the Attacker is to reach a state labeled as an accepting node; the goal of the Defender is to thwart the Attacker by preventing the Attacker from ever reaching an accepting node. The game is played in turns: on each turn, if the state is an Attacker state, then the Attacker can change the state to any adjacent node of the graph, and analogously for Defender states and Defender-initiated state changes. A winning Defender strategy for a game is a decision tree of choices that the Defender can make so that an accepting state is never reached. The core of a policy weaver created by our weaver generator is an algorithm to find a winning Defender strategy [HJR12]. A policy weaver generated by the policy-weaver generator works as follows: given program P and policy R, the policy weaver constructs a game in which
We have also been working on applying policy weaving to JavaScript programs. JavaScript is the most popular language used to create dynamic content for web browsers. Moreover, the nature of the Web has resulted in an ecosystem in which JavaScript programs and libraries, often written by untrusted third parties, are regularly incorporated into applications and combined in every way imaginable. While this practice has obvious benefits in terms of convenience and not ``reinventing the wheel,'' it creates glaring security holes because of a complete lack of isolation between modules in a JavaScript environment. We chose this context to apply our policy-weaving techniques because of the obviously unfilled need for a security mechanism, and because of the challenge presented by JavaScript's highly dynamic, untyped nature. We have created the the JAM policy weaver [FJJRPSY12], coupled with the JAMScript enforcement mechanism. (``JAM'' stands for JAvascipt Model checker.) JAM can be used by a website administrator to apply a security policy—in the form of a finite-state automaton—that specifies a set of disallowed execution traces of a JavaScript program. The program is analyzed statically with respect to the policy, and an instrumented program that is guaranteed to not violate the policy specification is produced. This analysis consists of a counterexample-guided, abstraction-refinement loop that repeatedly creates an incrementally more precise abstract model of the program. Because this model represents a superset of the program's actual behaviors, we can say that any execution traces that are not realizable in the model also cannot happen in the concrete program. Static analysis can be expensive, especially in the context of a highly dynamic language such as JavaScript. Thus, the algorithm used in JAM provides for a system-resource cutoff threshold, which terminates the analysis when the threshold is reached. This case still results in a safely instrumented program, although the program may contain some amount of spurious instrumentation, resulting in extra runtime overhead. In this way, JAM can be tuned to balance the trade-off between static-analysis overhead and dynamic overhead. The instrumentation that JAM weaves into a JavaScript program comes in the form of transactions. Potentially malicious statements in the untrusted code (i.e., those that could not be proven safe by the static analysis) are wrapped in transaction blocks, which are speculatively executed in a manner that records all actions (reads, writes, and function calls) and suppresses all effects of the actions. This approach allows the effects of the statements to be evaluated with respect to the security policy, at run-time inside the transaction. The program is terminated—without the effects of the actions being visible externally—if it is determined that any prefix of the sequence of actions will violate the policy. If no policy-violating action sequence is observed, the transaction is committed, and execution continues as before.
Incremental ComputingThe attribute-updating algorithm that I developed as part of my Ph.D. research [R82, RTD83, R84] is an example of an "incremental updating algorithm"—an algorithm that makes use of the solution to one problem instance I1 to find the solution to a nearby problem instance I2, where I2 is created by making a small change to problem instance I1. Over the years, I have encountered such problems in a variety of contexts, including interactive program-development environments [R82, RTD83, R84, RMT86, R88], dynamic graph problems [RR94a, RR94b, RR96a, RR96b], the construction of abstract transformers for program-analysis problems [RSL03, RSL10, EGR10], and propagation strategies in dataflow-analysis solvers [RSJM05]. My interest in incremental computing also led me to look at ways of transforming a program that computes a function F(x) on floating-point numbers into programs that compute good approximations to the derivative F'(x), the first divided difference F[x0,x1], Taylor-series expansions of F(x), and higher-order divided differences of F(x), as well as multivariate versions of such transformations [RR00, RR03] (see computational differentiation and computational divided differencing). Incremental computing was the subject of G. Ramalingam's Ph.D. dissertation [R96]. The incremental algorithm for the dynamic shortest-hyperpath problem in directed hypergraphs that my student G. Ramalingam and I developed [RR96b] has been used by AT&T to improve the performance of Open Shortest Path First (OSPF), the most commonly used Internet intra-domain routing protocol. The incremental shortest-hyperpath algorithm is used as a subroutine in a heuristic search algorithm for optimizing OSPF weights (for a given set of projected demands) and thereby reduce congestion [FT04]. The speed-up obtained by using our incremental algorithm was reported to be a factor of 15 to 20. In 2004, Mikkel Thorup told me that AT&T was using their results to adjust capacities in the AT&T network when they had to schedule link downtimes for maintenance. Apparently this happens quite frequently: he indicated that on the order of a dozen links had to be serviced each day. More recently, the ideas used in [RR96b] were combined with the A* search algorithm from the field of AI planning to create several incremental versions of A* search. These algorithms were used to solve planning problems and generate dynamically constrained trajectories for the full-size SUV of CMU's Tartan Racing Team, which won the DARPA 2007 Urban Challenge race for autonomous vehicles.
Computational Differentiation and Computational Divided DifferencingTools for computational differentiation transform a program that computes a numerical function F(x) into a related program that computes F'(x) (the derivative of F). Louis Rall (of the UW Mathematics Department) and I described how techniques similar to those used in computational-differentiation tools can be used to implement other program transformations—in particular, a variety of transformations for computational divided differencing [RR00, RR03], including multivariate versions of such transformations.
Representing Boolean and Pseudo-Boolean FunctionsIn summer 2018, Meghana Sistla visited the University of Wisconsin, supported by the S.N. Bose Scholars Program, and we worked to resurrect an idea of mine from the late 90s that had been rejected by the USPTO in 2002. The idea was for a plug-compatible replacement for BDDs for representing Boolean and pseudo-Boolean functions, called CFLOBDDs (for ``Context-Free Language Ordered Binary Decision Diagrams''). The key insight behind CFLOBDDs is that sub-decision-diagrams can be treated as standalone ``procedures,'' which allows additional reuse opportunities compared to BDDs. In the best case, one can obtain double-exponential compression compared to decision trees—i.e., an extra exponential factor over (quasi-)BDDs.Meghana joined Swarat Chaudhuri's research group at UT-Austin, and we have been continuing the work with Swarat. 25 years ago, I never found a compelling application where CFLOBDDs beat BDDs, but in the last few years we have found that CFLOBDDs can be quite good for simulating quantum circuits [SCR24]. The implementation is available at this [link]. Our Quasimodo tool for quantum simulation, which supports BDDs, Weighted BDDs, and CFLOBDDs, is available on GitHub at this link [link], and described in a CAV23 tool paper [SCR23a]. We have also developed a weighted version of CFLOBDDs, called WCFLOBDDs [SCR23b].
|
