Lucas Waye

About Me

I currently maintain and enhance TiVo's data analytics architecture. In my spare time I work on Whip, a contract monitor for microservices. Previously I worked on the backend for Timeful (acquired by Google) and on Hulu's analytics platform. I received a Ph.D. and Master's degree from Harvard under the guidance of Stephen Chong and a Bachelor's degree from Cornell.

Publications Distribution Security Privacy

The majority of my time as a computer scientist has been spent on communicating my ideas (in emails, meetings, presentations, design reviews, etc.) rather than actually developing them. Here you can find my published write-ups of some of what I have worked on in the past.

Click on one of the buttons above to see my publications on that topic.

  1. Cryptographically secure information flow control on key-value stores , CCS 2017 (with Pablo Buiras, Owen Arden, Alejandro Russo, and Stephen Chong)
    An extension to LIO that automatically and correctly uses cryptography when interacting with an untrusted store

    abstract: We present Clio, an information flow control (IFC) system that transparently incorporates cryptography to enforce confidentiality and integrity policies on untrusted storage. Clio insulates developers from explicitly manipulating keys and cryptographic primitives by leveraging the policy language of the IFC system to automatically use the appropriate keys and correct cryptographic operations. We prove that Clio is secure with a novel proof technique composing cryptographic proof techniques with standard programming language techniques. We present a prototype Clio implementation along with a case study that demonstrates Clio's practicality.
    Lucas Waye, Pablo Buiras, Owen Arden, Alejandro Russo and Stephen Chong
    In Proceedings of the 24th ACM Conference on Computer and Communications Security (CCS), October 2017.
    [Paper | arXiv (with proofs) | Artifact]
  2. Composable enhancements for gradual assurances , Ph.D. dissertation, Harvard University, June 2017.
    A presentation of Whip, Clio, and restricted privileges

    abstract: This dissertation presents three enhancements to software components that increase the trustworthiness and usability of the systems they comprise. The enhancements are composable: they are local to the components they enhance and are self-contained. Since they are self-contained and local, composable enhancements can be partially deployed in a system without adversely affecting system behavior. The assurances provided by the enhancements are gradual: as the number of enhanced components in the system increases, the overall assurances provided by the entire system also increases. This dissertation investigates these enhancements in three different settings. In each setting, it identifies an inherent security or functional correctness problem with the components in that setting and provides a composable enhancement that remedies the problem gradually.

    In the first setting, this dissertation identifies that although modern services expose interfaces that are higher-order in spirit, the simplicity of the network protocols used forces services to rely on brittle encodings. To bridge the semantic gap, this dissertation presents Whip, a higher-order contract system that allows programmers to detect when services do not live up to their advertised higher-order interfaces. As more services use Whip, it becomes easier to identify errant services in the system.

    In the second setting, this dissertation identifies that in the Disjunction Category label model, capability-like privileges are used to downgrade information, which when used inappropriately can compromise security. To ensure privileges are used as intended, this dissertation presents restricted privileges, an enhancement to privileges to control downgrading based on a specification of security conditions for when they can be legitimately used. As more privileges are restricted, information in the system becomes more protected from the accidental or malicious exercise of privileges to downgrade more information than intended.

    In the third setting, this dissertation identifies that information-flow control (IFC) programs often need to interact with a key-value store that can also be accessed by non-IFC programs. These non-IFC programs may inadvertently (or maliciously) fail to respect the policies enforced by the IFC programs. In order to ensure the information protected by the IFC programs is not exfiltrated or corrupted by non-IFC programs through the key-value store, this dissertation presents Clio, an extension to a popular IFC language that transparently incorporates cryptography for data on the untrustworthy key-value store. As more IFC programs use Clio, the more information is protected from non-IFC programs in the system.

    Lucas Waye. Harvard University, Ph.D. dissertation, June 2017.
    [Dissertation]
  3. Whip: Higher-order contracts for modern services , ICFP 2017 (with Christos Dimoulas and Stephen Chong)
    A run-time software contract monitor for microservices

    abstract: Modern service-oriented applications forgo semantically rich protocols and middleware when composing services. Instead, they embrace the loosely-coupled development and deployment of services that communicate via simple network protocols. Even though these applications do expose interfaces that are higher-order in spirit, the simplicity of the network protocols forces them to rely on brittle low-level encodings. To bridge the apparent semantic gap, programmers introduce ad-hoc and error-prone defensive code. Inspired by Design by Contract, we choose a different route to bridge this gap. We introduce Whip, a contract system for modern services. Whip (i) provides programmers with a higher-order contract language tailored to the needs of modern services; and (ii) monitors services at run time to detect services that do not live up to their advertised interfaces. Contract monitoring is local to a service. Services are treated as black boxes, allowing heterogeneous implementation languages without modification to services' code. Thus, Whip does not disturb the loosely coupled nature of modern services.
    Lucas Waye, Christos Dimouas, and Stephen Chong
    In Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2017.
    [Paper | Presentation Video | Artifact | Appendices | Website]
  4. Flexible manipulation of labeled values for information-flow control libraries , ESORICS 2016 (with Marco Vassena, Pablo Buiras, and Alejandro Russo)
    Allow secure computation on labeled values in IFC systems without unlabeling by using the functor structure and applicative operator

    abstract: The programming language Haskell plays a unique, privileged role in Information-Flow Control (IFC) research: it is able to enforce information security via libraries. Many state-of-the- art libraries (e.g., LIO, HLIO, and MAC) allow computations to manipulate data with different security labels by introducing the notion of labeled values, which protect values with explicit labels by means of an abstract data type. While computations have an underlying algebraic structure in such libraries (i.e. monads), there is no research on structures for labeled values and their impact on the programming model. In this paper, we add the functor structure to labeled values, which allows programmers to conveniently and securely perform computations without side-effects on such values, and an applicative operator, which extends this feature to work on multiple labeled values combined by a multi- parameter function. This functionality simplifies code, as it does not force programmers to spawn threads to manipulate sensitive data with side-effect free operations. Additionally, we present a relabel primitive which securely modifies the label of labeled values. This operation also helps to simplify code when aggregating data with heterogeneous labels, as it does not require spawning threads to do so. We provide mechanized proofs of the soundness our contributions for the security library MAC, although we remark that our ideas apply to LIO and HLIO as well.
    Marco Vassena, Pablo Buiras, Lucas Waye, and Alejandro Russo
    In Proceedings of the 21st European Symposium on Research in Computer Security (ESORICS), September 2016.
    [Paper]
  5. It's my privilege: controlling downgrading in DC-labels , STM 2015 (with Pablo Buiras, Dan King, Stephen Chong, and Alejandro Russo)
    The use of privileges in IFC systems can be limited to prevent their misuse by restricting where in the security lattice they may be used and who may influence their use.

    abstract: Disjunction Category Labels (DC-labels) are an expressive label format used to classify the sensitivity of data in information-flow control systems. DC-labels use capability-like privileges to downgrade information. Inappropriate use of privileges can compromise security, but DC-labels provide no mechanism to ensure appropriate use. We extend DC-labels with the novel notions of bounded privileges and robust privileges. Bounded privileges specify and enforce upper and lower bounds on the labels of data that may be downgraded. Bounded privileges are simple and intuitive, yet can express a rich set of desirable security policies. Robust privileges can be used only in downgrading operations that are robust, i.e., the code exercising privileges cannot be abused to release or certify more information than intended. Surprisingly, robust downgrades can be expressed in DC-labels as downgrading operations using a weakened privilege. We provide sound and complete run-time security checks to ensure downgrading operations are robust. We illustrate the applicability of bounded and robust privileges in a case study as well as by identifying a vulnerability in an existing DC-label-based application.
    Lucas Waye, Pablo Buiras, Dan King, Stephen Chong, and Alejandro Russo
    In Proceedings of the 11th International Workshop on Security and Trust Management (STM), September 2015.
    [Paper | Slides]
  6. Exploring and enforcing security guarantees via program dependence graphs , PLDI 2015 (with Andrew Johnson, Scott Moore, and Stephen Chong)
    A program analysis and understanding tool that enables the specification and enforcement of precise application-specific information security guarantees

    abstract: We present Pidgin, a program analysis and understanding tool that enables the specification and enforcement of precise application-specific information security guarantees. Pidgin also allows developers to interactively explore the information flows in their applications to develop policies and investigate counter-examples.

    Pidgin combines program-dependence graphs (PDGs), which precisely capture the information flows in a whole application, with a custom PDG query language. Queries express properties about the paths in the PDG; because paths in the PDG correspond to information flows in the application, queries can be used to specify global security policies.

    Pidgin is scalable. Generating a PDG for a 335k line Java application takes under 90 seconds, and checking each of our policies on that PDG takes under 14 seconds. The query language is expressive, supporting a large class of precise, application-specific security guarantees. Policies are separate from the code and do not interfere with testing or development, and can be used for security regression testing.

    We describe the design and implementation of Pidgin and report on using it: (1) to explore information security guarantees in legacy programs; (2) to develop and modify security policies concurrently with application development; and (3) to develop policies based on known vulnerabilities.

    Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong
    In Proceedings of the 36th ACM SIGPLAN Conference on Programming Langauge Design and Implementation (PLDI), June 2015.
    [Paper | Website]
  7. Privacy integrated data stream queries , PSP 2014
    A practical framework for which a non-expert can perform differentially private operations on data streams

    abstract: Research on differential privacy is generally concerned with examining data sets that are static. Because the data sets do not change, every computation on them produces "one-shot" query results; the results do not change aside from randomness introduced for privacy. There are many circumstances, however, where this model does not apply, or is simply infeasible. Data streams are examples of non-static data sets where results may change as more data is streamed. Theoretical support for differential privacy with data streams has been researched in the form of differentially private streaming algorithms. In this paper, we present a practical framework for which a non-expert can perform differentially private operations on data streams. The system is built as an extension to PINQ (Privacy Integrated Queries), a differentially private programming framework for static data sets. The streaming extension provides a programmatic interface for the different types of streaming differential privacy from the literature so that the privacy trade-offs of each type of algorithm can be understood by a non-expert programmer
    Lucas Waye
    In Proceedings of the 1st International Workshop on Privacy and Security in Programming (PSP), October 2014.
    [Paper | Slides | GitHub]
  8. Framework for generating programs to process beacons , US Patent (with Kevin Seng, Viral Bajaria, and Shane Moriah)
    A translator from high-level, declarative beacon specifications to programs that process and validate those beacons

    abstract: A method receives a specification for processing beacons. The beacons are associated with an event occurring at a client while a user is interacting with a web application and include unstructured data. The method parses the specification to determine an object model including objects determined from the specification where different specifications are parsed into a format of the object model. A generator is determined and each generator is configured to process the format of the object model to generate a different type of target program to process the beacons and multiple generators can process different specifications that are parsed into the format of the object model. The method runs the generator with the object model to generate a target program configured to identify the beacons for the specification, determine unstructured data in the beacons that were specified in the specification, and transform the unstructured data into structured data.
    Lucas Waye, Kevin Seng, Viral Bajaria, and Shane Moriah
    US Patent 8,725,750. May 2014.
    [Google Patent | Blog Post]
  9. Fabric: A platform for secure distributed computation and storage , SOSP 2009 (with Jed Liu, Michael D. George, K. Vikram, Xin Qi, and Andrew C. Myers)
    A high-level programming language for building open distributed applications with strong security

    abstract: Fabric is a new system and language for building secure distributed information systems. It is a decentralized system that allows heterogeneous network nodes to securely share both information and computation resources despite mutual distrust. Its high-level programming language makes distribution and persistence largely transparent to programmers. Fabric supports data-shipping and function-shipping styles of computation: both computation and information can move between nodes to meet security requirements or to improve performance. Fabric provides a rich, Java-like object model, but data resources are labeled with confidentiality and integrity policies that are enforced through a combination of compile- time and run-time mechanisms. Optimistic, nested transactions ensure consistency across all objects and nodes. A peer-to-peer dissemination layer helps to increase availability and to balance load. Results from applications built using Fabric suggest that Fabric has a clean, concise programming model, offers good performance, and enforces security.
    Jed Liu, Michael D. George, K. Vikram, Xin Qi, Lucas Waye, and Andrew C. Myers
    In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), October 2009.
    [Paper | Website]

Interests

I served as a teaching assistant for a few courses focusing on various topics from programming languages: undergraduate-level compilers (CS 153 at Harvard in Fall 2013 where I was awarded a certificate for distinction in teaching), functional programming (CS 3110 at Cornell in Spring 2011, Fall 2010, and Fall 2009), up to a graduate-level seminar course in advanced topics (CS 252r at Harvard in Fall 2015).

While in graduate school I consulted in my spare time and received the Rising Star award from DARPA for some of my work.

Take a look at my National Parks Checklist to see the extent to which I've enjoyed "America's best idea."

National Parks Checklist

Work Experience

TiVo
TiVo
Associte Big Data Architect
STR
STR
Software Consultant
Timeful
Timeful
Backend Developer
Hulu
Hulu
Software Developer
Amazon.com
Amazon.com
Software Developer Intern