Track: Modern CS in the Real World

Category Theory for the Working Hacker

The talk will explain why category theory is of interest for developers. The principle of Propositions as Types describes a correspondence between, on the one hand, propositions and proofs in logic, and, on the other, types and programs in computing. And, on the third hand, we have category theory! Assuming only high school maths, the talk will explain how categories model three basic data types: products (logical and), sums (logical or), and functions (logical implication). And it explains why you already learned the most important stuff in high school.

Abstractions to Help Developers Write Good Crypto

More developers are writing cryptographic code, especially in regulated sectors like health care and financial services, but the code suffers from a combination of poor programming interfaces and a lack of developer training. In one study, 83% of cryptographic flaws (CVEs) were due to programmer misuse of otherwise correct libraries. While solutions like LetsEncrypt have made HTTPS cheaper, encryption of data in transit only covers a small part of the problem space. End-to-end crypto is an important approach, and is getting more widespread, but can programmers implement it securely?

In this talk, we will discuss the impact of programming abstractions on the correctness of cryptographic code, and show why some cryptographic libraries succeed in helping the programmers Do The Right Thing, and why some fail.

Logic-Based Automated Reasoning

Developing efficient and scalable software analysis tools is a tedious and very difficult task. First, due to the undecidability of the verification problem, tools, must be highly tuned and engineered to provide reasonable efficiency and precision trade-offs. Second, different programming languages come with very diverse assortments of syntactic and semantic features. Third, the diverse encoding of the verification problem makes the integration with other powerful solvers and verifiers difficult. In this talk, I will present SeaHorn — an open source automated logic-based reasoning tool built on top of LLVM -- an industrial compiler infrastructure. SeaHorn combines traditional and advanced automated reasoning algorithms based on Satisfiability Modulo Theory (SMT) and Abstract Interpretation. SeaHorn is a versatile and highly customizable tool which allows developers to easily build or experiment with new verification techniques.

Real-Time Collaborative Editing with CRDTs

Real-time collaborative editing gives users the illusion that they are editing the same document, but in reality, each collaborator makes edits to their own local replica of the document to ensure a low-latency typing experience. Each user's local operations must then be transmitted to remote collaborators and integrated so that the contents of every replica remain equivalent and that the intentions behind each participant's edits are preserved. This challenge has been the focus of nearly three decades of ongoing research in the field of operational transformation, which has produced various algorithms with different trade-offs that are notoriously difficult to implement. In 2011, a new conceptual framework called conflict-free replicated data types (CRDTs) emerged to offer a significantly simpler approach to collaborative text editing and related distributed computing problems. In this talk, we'll explore a new library that draws from the latest CRDT research to enable real-time collaborative text editing in a fully distributed setting.

Modern CS in the Real World Open Space

Programming the Network Data Plane

We all know how to program CPUs, making it easy to prototype new ideas, build new applications, and share them with others. Today it is commonplace to program not just CPUs, but almost any domain-specific processors, such as GPUs, DSPs, and even machine-learning accelerators (e.g., TPUs). Unfortunately networking has long been an exception to this trend; the network data plane -- packet processing -- has been dictated by fixed-function switching chips, which help up innovations in the fields of networking, computing, and storage all together.

But this is changing quickly. The new PISA (Protocol-Independent Switch Architecture) ASICs promise multi Tb/s of packet processing with uncompromised programmability. P4, a new domain-specific high-level language designed for networking, additionally allows network engineers and developers to program PISA chips and other types of programmable packet-processing devices (e.g., FPGAs, NPUs, and S/W switches) in a declarative and intuitive fashion. PISA and P4 will entirely change the way people design, build, and run not just their networks, but their distributed systems and applications as well.

In this talk, I’ll first explain what PISA and P4 are, how they work, what kinds of design principles they are built on, and why they are made possible now. I’ll also introduce a few killer applications of these technologies. Then I’ll characterize PISA as a “relentless I/O-event execution machine” and show how this characterization opens up possibilities for joint-engineering a network and the distributed applications running on the network. I’ll conclude my talk by introducing a few such exciting examples.