These abstracts are for talks at this event.
NEPLS is a venue for ongoing research, so the abstract and supplemental material associated with each talk is necessarily temporal. The work presented here may be in a state of flux. In all cases, please consult the authors' Web pages for up-to-date information. Please don't refer to these pages as a definitive source.
Sainyam Galhotra (UMass Amherst)
Today, software is making more automated decisions with societal impact, and so it becomes critical to ensure that the software acts fairly. For example, software determines who gets a loan and who gets hired, and it is being used at every stage of the criminal justice system, including computing risk-assessment scores that help determine who goes to jail and who is set free. Toward that end, we define a novel measure of software discrimination that captures causal relationships between sensitive input attributes and software behavior. Our approach, Themis, measures discrimination in software by generating efficient, discrimination-testing test suites that, importantly, do not need an oracle. We evaluate Themis on 20 software systems, some of which come from prior work with explicit focus on avoiding discrimination. We find that (1) Themis is effective at discovering software discrimination, (2) state-of-the-art techniques for removing discrimination from algorithms fail in many situations, at times discriminating against as much as 98% of an input subdomain, (3) Themis optimizations are effective at producing efficient test suites for measuring discrimination, and (4) Themis is more efficient on systems that exhibit more discrimination. We thus demonstrate that fairness testing is a critical aspect of the software development cycle in domains with possible discrimination and provide initial tools for measuring software discrimination.
Decomposition Instead of Self-Composition for Proving the Absence
of Timing Channels
Paul Gazzillo (Yale University)
We present a novel approach to proving the absence of timing channels. The idea is to partition the program's execution traces in such a way that each partition component is checked for timing attack resilience by a time complexity analysis and that per-component resilience implies the resilience of the whole program. We construct a partition by splitting the program traces at secret-independent branches. This ensures that any pair of traces with the same public input has a component containing both traces. Crucially, the per-component checks can be normal safety properties expressed in terms of a single execution. Our approach is thus in contrast to prior approaches, such as self-composition, that aim to reason about multiple k <= 2 executions at once. We formalize the above as an approach called quotient partitioning, generalized to any $k$-safety property, and prove it to be sound. A key feature of our approach is a demand-driven partitioning strategy that uses a regex-like notion called trails to identify sets of execution traces, particularly those influenced by tainted (or secret) data. We have applied our technique in a prototype implementation tool called Blazer, based on WALA, PPL, and the brics automaton library. We have proved timing-channel freedom of (or synthesized an attack specification for) 24 programs written in Java bytecode, including 6 classic examples from the literature and 6 examples extracted from the DARPA STAC challenge problems.
Artifacts for Semantics: An OCaml Experiment
Daniel Patterson (Northeastern University)
We present a brief experience report and demonstration of an artifact we built for a semantics paper. The paper presents a multi-language that incorporates a typed assembly language (TAL) and a simple functional language where each can be embedded within the other. The artifact is an online editor, type-checker, and stepper that allowed readers to run examples from the paper, write their own programs, and in general experiment with the multi-language. We think it was successful both as a tool to aid readers, but it also helped us to ensure our examples were correct and that there were not typos in the presentation of the formalism. Given the low effort to construct such an artifact (as compared to, for example, formalizing the results in a theorem prover), we think this approach is worth considering for other authors. For more information, see http://prl.ccs.neu.edu/blog/2017/05/15/artifacts-for-semantics/ The talk will be a brief summary of the approach, and then a short demo of the artifact.
Web-based Debugging for Free
Sam Baxter and Rachit Nigam (UMass Amherst)
Automated System Configuration Repair
Aaron Weiss (UMass Amherst)
Modern system configuration languages provide powerful abstractions that make system administration easier. These languages are widely used. For example, over 33,000 organizations use Puppet, including 75 of the Fortune 100. Still, configuration scripts often contain bugs and the shell is the simplest way to diagnose them. Unfortunately, fixing bugs from the shell is unsafe as it causes the system to drift from the state specified in the script. Thus, configuration languages, despite their advantages, force system administrators to give up the simplicity and familiarity of the shell. This talk will present a synthesis-based technique that allows administrators to use configuration languages and the shell in harmony. We allow administrators to fix errors from the shell and the technique automatically repairs the high-level configuration script to stay in sync. The approach (1) produces sound repairs, (2) produces maintainable repairs, (3) ranks and presents multiple repairs when relevant, and (4) supports any shell. We've implemented our approach for Puppet, the most widely used system configuration language. We evaluate our system on existing benchmarks under 42 repair scenarios. We find that the top-ranked repair is selected by humans 76% of the time and that the human-equivalent repair is ranked 1.310 on average.
Static Detection of Event-based Races in Android Apps
Yongjian Hu (UC Riverside) and Iulian Neamtiu (New Jersey Institute of Technology)
Event-based races are the predominant source of concurrency errors in Android apps. So far all the approaches for detecting event-based races have been dynamic. Due to their dynamic nature, these approaches suffer from coverage and false negative issues, and despite being dynamic they still have a high rate of false positives. We introduce a static approach and tool, named SIERRA, for detecting Android event-based races centered around a new concept of ``concurrency action'' (that reifies threads, events/messages, system and user actions) and statically-derived order (happens-before relation) between actions. Establishing action order is complicated in Android, and event-based systems in general, because of externally-orchestrated control flow, use of callbacks, asynchronous tasks, and ad-hoc synchronization. Our approach introduces several key enablers for inferring order relations statically: models which impose order among lifecycle and GUI events; static analysis refinements, e.g., path-sensitive pointer analysis; and finally, on-demand path sensitivity via backward symbolic execution to further rule out false positives. We evaluate SIERRA on 194 Android apps. Of these, we chose 20 apps for manual analysis and comparison with a dynamic race detector. Experimental results show that our approach is effective and efficient, typically taking 1,230 seconds to analyze an app and revealing 33 potential races. Moreover, SIERRA can refute false positive races reported by the dynamic detector. Our approach opens the way for precise analysis and static event race detection in other event-driven systems beyond mobile platforms.
Generic Coq Library for Certified Static Checking of Module-like
Julia Belyakova (Southern Federal University, Russia)
As a means of abstraction, many programming languages provide some sort of module-like constructs. Examples are interfaces in object-oriented languages, signatures in ML, type classes in Haskell. All of these constructs share some common properties: they define pairs of "interface" and "implementation" components (e.g. interfaces and classes, signatures and modules), introduce namespaces, and obey some high-level notions of well-definedness. For instance, we can consider an "implementation" as well-defined if all of its members are well-defined, and all members required by a corresponding "interface" are defined. At the same time, there are various ways to check that the members are well-defined. For example, it may be enough to take into account only previously defined members when checking the current one (as in ML-module without mutual recursion); or it may be the case that all members are considered at every point (as in Java-class). Also, checking well-definedness of a self-contained class may be different from checking of a class, which extends another one. In this talk we present an ongoing work on the generic Coq library for certified static checking of module-like constructs of different flavours. It is intended to be used in certified compilers/interpreters, which seek for both efficient representation of language constructs and easiness-to-reason-about them. The library defines three building blocks for several concrete notions of modules. The first one, propositional, provides definitions of well-definedness; the second one, computational, implements efficient algorithms for checking modules; and the third one provides proofs of correctness of algorithms (from the second block) with respect to the propositional definitions (the first block).
Copattern-matchings and first-class observations at Work
Paul Laforgue (Northeastern University & Diderot University)
Infinite data structures are elegantly defined using copattern-matching, a dual construction to pattern-matching that expresses the outcomes of the observations of an infinite object. We extended the OCaml programming language with copatterns, exploiting the duality between pattern-matching and copattern-matching. Provided that a functional programming language has GADTs, every copattern-matching can be transformed into a pattern-matching via a purely local syntactic transformation, a macro. The development of this extension leads us to a generalization of previous calculus of copatterns: the introduction of first-class observation queries. During this talk, we will demonstrate how codata types and copatterns help to understand and manipulate the infinite in a more natural way. We will implement infinite objects, starting with streams and ending with more sophisticated ones, such as the implementation of the game of life using an infinite zipper.
Gradual Types for Objects Redux
Benjamin Chung (Northeastern University)
The ideal of gradual typing is to add types to untyped languages, a motivation that researchers have taken up with great enthusiasm, developing a wide range of approaches for combining sound types with untyped code. However, these new techniques are typically presented for a specific language and inherit all the complexity of that language, muddying comparisons, making extension more difficult, and obscuring potential implementations. To clarify the differences between the approaches and to allow extension to new languages, we present a common, object-oriented, core calculus for gradual typing inspired by the CIL, called KafKa, and translations to KafKa from several notable gradual type systems, including Typed Racket, Thorn, and the Transient semantics in Reticulated Python. By using a commodity VM inspired core calculus, we simultaneously illustrate implementation approaches for gradually typed programming languages, while simultaneously highlighting the semantics of each approach in the translations.
Debugging Memory Safety Errors in Memory Managers
Karl Cronburg (Tufts University)
Debugging a memory manager is hard. While general purpose tools exist to alleviate the debugging effort, such as GDB and Valgrind, we believe such tools do not sufficiently support debugging of memory managers. In this talk, I will present a new approach to debugging memory managers based on a high-level specification language coupled with binary instrumentation. Of particular importance to debugging a memory manager is how it operates. Memory managers operate by allocating memory according to a stratified protocol whereby memory tran- sitions across different layers. For example, the Glasgow Haskell Compiler's (GHC's) memory manager allocates memory into layers named megablock, block, and object. At each layer memory managers also bifurcate the memory into allocated and free states: a GHC block can be either allocated or free.
Measuring Reticulated Python
Ben Greenman (Northeastern University)
Is sound gradual typing dead? In the context of Typed Racket, a gradual type system that guarantees "classic" type soundness, the cost of enforcing soundness at runtime is high. Reticulated is an implementation of gradual typing for Python. It provides an alternative soundness guarantee that requires less runtime overhead to enforce. This talk will explain Reticulated's notion of soundness, question its practicality, and report our findings on Reticulated's performance.
Finding Optimal Schedules for Generational Garbage Collectors
Nicholas Jacek (UMass Amherst)
In a generational garbage collector, the cost of performing a collection varies with the amount of data that is live and with the specific objects that have been promoted - and thus is influenced by the past sequence of collections. By carefully choosing the times when a collection is performed, the overall cost of running the garbage collector can be reduced. To this end, we present a dynamic program that, given an after-the-fact trace of a program's execution on a Java virtual machine, finds the schedule of major and minor collections that has the minimum possible cost. We then give results that compare optimal and naive schedules on the DaCapo benchmarks using a wide range of young space and old space sizes. We also compare with lower and upper bounds on the optimal that are potentially even cheaper to compute. Surprisingly we find that in practice these bounds are often tight, which may offer further insight into optimal GC cost. We also hope to include some measurements of the cost to compute optimal schedules using our dynamic program written in the Julia programming language. This is an update to our prior work. Previously, we had used reinforcement learning techniques to find near-optimal schedules. However, these were only approximately optimal, since finding exactly optimal schedules would take exponential time. Our new reformulation of the problem as a dynamic program allows us to find exactly optimal schedules in feasible amounts of time, a significant improvement. Work in progress that we expect to submit for journal publication this summer.
Tracking the Provenance of Machine Learning Models
Nathan Ricci (Microsoft)
We present preliminary work on tracking the origins of machine learning programs. Our system takes unmodified Apache Spark programs, applies dynamic instrumentation, and produces a data structure recording what files, which functions, what parameters were used to generate models(along with what other outputs the program nomrally produces), with minimal over head.
|Last modified Friday, June 2nd, 2017 8:50:14pm|