[pl-seminar] Two talks Friday, 3pm, 4310

[Evan Driscoll <driscoll@xxxxxxxxxxx>]

Sorry for the late notice, but there are two practice talks for CAV on Friday 
at 3pm in 4310. The first listed is a short (5 minute) tool talk.


OpenNWA: A Nested-Word-Automaton Library
Evan Driscoll, Aditya Thakur, and Thomas Reps
(talk by Evan Driscoll)

    Abstract. Nested-word automata (NWAs) are a language formalism
    that helps bridge the gap between finite-state automata and push-
    down automata. NWAs can express some context-free properties, such as
    parenthesis matching, yet retain all the desirable closure characteristics
    of finite-state automata.

    This paper describes OpenNWA, a C++ library for working with
    NWAs. The library provides the expected automata-theoretic operations,
    such as intersection, determinization, and complementation. It is pack-
    aged with WALi—the Weighted Automaton Library—and interoperates
    closely with the weighted pushdown system portions of WALi.


Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction 
Refinement
Matthew Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps, Phillip Porras, 
Hassen Saïdi, and Vinod Yegneswaran
(talk by Richard Joiner)

    Abstract. Stateful security policies—which specify restrictions on 
    behavior in terms of temporal safety properties—are a powerful tool for 
    administrators to control the behavior of untrusted programs. However, the 
    runtime overhead required to enforce them on real programs can be high. 
    This paper describes a technique for rewriting programs to incorporate 
    runtime checks so that all executions of the resulting program either 
    satisfy the policy, or halt before violating it. By introducing a 
    rewriting step before runtime enforcement, we are able to perform static 
    analysis to optimize the code introduced to track the policy state. We 
    developed a novel analysis, which builds on abstraction-refinement 
    techniques, to derive a set of runtime policy checks to enforce a given 
    policy—as well as their placement in the code. Furthermore, the 
    abstraction refinement is tunable by the user, so that additional time 
    spent in analysis results in fewer dynamic checks, and therefore more 
    efficient code. We report experimental results on an implementation of the 
    algorithm that supports policy checking for JavaScript programs.