MACS Project Meeting, December 2018

Date:
Friday, December 7, 2018

Location:
MIT, Star conference room (32-D463) in the Stata Center at 32 Vassar St, Cambridge, MA

Schedule:

Abstracts:

Sahil Tikale and Amin Mosayyebzadeh, Elastic Secure Marketplace for Trading Bare-metal Servers

We describe our research efforts towards building a marketplace where different stakeholders from academia, research and industry can trade their bare-metal servers when they have excess capacity to spare or when others need it more than them. The talk discusses the need for such a marketplace where many stakeholders, rather than just a single provider, participate in standing up and operate a multi-cloud infrastructure. We will talk about the different microservices namely HIL, M2, Bolted and FLOCX that we have developed as a part of our research that collectively contribute to this vision.

HIL is a fundamental new layer that decouples allocation of bare-metal servers from the solutions required for deploying OS and applications. It lets users move hardware resources between different owners and different provisioning systems as elastically as new VMs are spinned up in the cloud.

To match the rapid rate of allocation, we developed M2 that lets you set up the cluster from bare-metal to workload ready in matter of minutes. It uses remotely mounted OS images making it possible to use bare-metal servers like VMs that can be migrated with minimal loss of state.

Bolted is an effort to carve out a secure group of bare-metal servers from a potentially non-secure pool of hardware such that the tenant can verify the integrity from bios to the application at each step of deployment. It gives the choice to the tenants on the level of security they wishes to implement.

Lastly we describe FLOCX — an economic model to incentive sharing of nodes between non-trusting tenants.

Hoda Maleki, Universal Composability Security Analysis of OpenStack

We initiate an effort to demonstrate how we can provide a rigorous, perceptible and holistic security analysis of OpenStack. OpenStack is the prevalent open-source, non-proprietary package for managing cloud services and data centers. It is highly complex and consists of multiple inter-related components which are developed by separate, loosely coordinated groups. All of these properties make the security analysis of OpenStack both a crucial mission and a challenging one. We base our modeling and security analysis in the universally composable (UC) security framework, which has been so far used mainly for analyzing the security of cryptographic protocols. Indeed, demonstrating how the UC framework can be used to argue about security-sensitive systems which are mostly non-cryptographic, in nature, is one of the main contributions of this work. Our analysis is user-centric, modular, extendable, and provides defense in depth. Although our analysis covers only a number of core components of OpenStack, it formulates some basic and important security trade-offs in the design. It also naturally paves the way to a more comprehensive analysis of OpenStack.

Alley Stoughton, Towards Modular, Mechanized Proofs of Cryptographic Protocol Security

We give an early status report on our research at marrying the universally composable (UC) security framework of theoretical cryptography with the EasyCrypt cryptographic proof assistant. The goal is to obtain a mechanized proof assistant and related tools enabling security proofs that are modular, and at the same time rigorous and cryptographically sound. The project is bridging the gap between the coroutine-based execution model of the UC framework and the traditional procedural execution model of EasyCrypt, and we plan to develop a domain-specific extension of the EasyCrypt programming language for representing UC protocols and security specifications, and to implement the UC composition operation and theorem within EasyCrypt.

Joint work with Ran Canetti, Assaf Kfoury and Mayank Varia

Atalay Mert Ileri, Proving confidentiality in a file system using DiskSec

SFSCQ is the first file system with a machine-checked proof of security. To develop, specify, and prove SFSCQ, this paper introduces DiskSec, a novel approach for reasoning about confidentiality of storage systems, such as a file system. DiskSec addresses the challenge of specifying confidentiality using the notion of data noninterference to find a middle ground between strong and precise information-flow-control guarantees and the weaker but more practical discretionary access control. DiskSec factors out reasoning about confidentiality from other properties (such as functional correctness) using a notion of sealed blocks. Sealed blocks enforce that the file system treats confidential file blocks as opaque in the bulk of the code, greatly reducing the effort of proving data noninterference. An evaluation of SFSCQ shows that its theorems preclude security bugs that have been found in real file systems, that DiskSec imposes little performance overhead, and that SFSCQ’s incremental development effort, on top of DiskSec and DFSCQ, on which it is based, is moderate.

Rawane Issa, Privacy Enhancing Route Recommendation

Route recommendation services (e.g. Google maps) have become widespread and incorporate numerous factors (e.g. traffic and road closures) to compute optimal routes. Utilizing these services, however, comes at a cost to user’s privacy: the service provider learns the source and destination locations of the user for every query that is submitted. Previous protocols for privacy preserving route recommendation algorithms have been constructed using tools such as garbled circuits and private information retrieval (PIR), but have had large overheads in latency and bandwidth.

In this work, we present an MPC protocol and architecture for route recommendation that guarantees: (1) low latency and bandwidth for user queries, (2) scalability with respect to the number of users, and (3) independence from the underlying route recommendation algorithm. We provide a differential privacy-esque extension to our protocol in order to provide meaningful guarantees against inference attacks. Our protocol extends to other applications of key-value PIR protocols.

This work is implemented using JIFF, an easy to use general-purpose framework for implementing MPC protocols in a contemporary web technology stack.

Daniel Wichs, Is there an Oblivious RAM Lower Bound for Online Reads?

Oblivious RAM (ORAM), introduced by Goldreich and Ostrovsky (JACM 1996), can be used to read and write to memory in a way that hides which locations are being accessed. The best known ORAM schemes have an O(logn) overhead per access, where n is the data size. The work of Goldreich and Ostrovsky gave a lower bound showing that this is optimal for ORAM schemes that operate in a “balls and bins” model, where memory blocks can only be shuffled between different locations but not manipulated otherwise. The lower bound even extends to weaker settings such as offline ORAM, where all of the accesses to be performed need to be specified ahead of time, and read-only ORAM, which only allows reads but not writes. But can we get lower bounds for general ORAM, beyond “balls and bins”?

The work of Boyle and Naor (ITCS ’16) shows that this is unlikely in the offline setting. In particular, they construct an offline ORAM with o(logn) overhead assuming the existence of small sorting circuits. Although we do not have instantiations of the latter, ruling them out would require proving new circuit lower bounds. On the other hand, the recent work of Larsen and Nielsen(CRYPTO ’18) shows that there indeed is an Ω(logn) lower bound for general online ORAM.

This still leaves the question open for online read-only ORAM or for read/write ORAM where we want very small overhead for the read operations. In this work, we show that a lower bound in these settings is also unlikely. In particular, our main result is a construction of online ORAM where reads(but not writes) have an o(logn) overhead, assuming the existence of small sorting circuits as well as very good locally decodable codes (LDCs). Although we do not have instantiations of either of these with the required parameters, ruling them out is beyond current lower bounds.

Alin Tomescu, Append-only Authenticated Dictionaries and Their Applications

Transparency logs allow users to audit a potentially malicious service, paving the way towards a more accountable Internet. For example, Certificate Transparency (CT) enables domain owners to audit Certificate Authorities (CAs) and detect impersonation attacks. Yet to achieve their full potential, transparency logs must be efficiently auditable. Specifically, everyone should be able to verify both (non)membership of log entries and that the log remains append-only. Unfortunately, current transparency logs either provide small-sized (non)membership proofs or small-sized append-only proofs, but never both. In fact, one of the proofs always requires bandwidth linear in the size of the log, making it expensive for everyone to audit the log and resulting in a few “opaque” trusted auditors. In this paper, we address this gap with a new primitive called an append-only authenticated dictionary (AAD). Our construction is the first to achieve (poly)logarithmic size for both proof types.

Alex Lombardi, Recent Progress on Fiat-Shamir in the Plain Model

The Fiat-Shamir heuristic provides a general template for transforming a public-coin interactive proof into a non-interactive argument: the verifier in a (many-round) interactive proof is replaced by a hash function that the prover can query non-interactively. It is well-known that this transformation is sound if the hash function is modeled as a random oracle, but it is a notorious open problem to show, for essentially any interactive protocol, that a concrete hash function family can be used instead.

For a long time, the goal of achieving Fiat-Shamir in the standard model seemed well out of reach, as exemplified by strong negative results. However, an exciting line of positive results in the last two years has shown that under very strong but plausible assumptions, instantiating the Fiat-Shamir heuristic in the plain model is possible. In this talk, I will survey some of these recent results, which aim to rely on both weaker and simpler computational assumptions.

This talk is based on joint work with Ran Canetti, Yilei Chen, Justin Holmgren, Guy Rothblum, and Ron Rothblum, as well as joint work with Ran Canetti and Daniel Wichs.

Prabhanjan Ananth, Round Optimal Secure Computation in the Honest Majority Setting

Secure multiparty computation allows for mutually distrustful parties to come together and jointly compute a function on their private inputs. The problem of realizing secure multiparty computation in the honest majority setting with minimal number of rounds has been open for almost three decades. In this talk, I will present two constructions of two-round secure multiparty computation protocols in the honest majority setting:

• Secure MPC for P/poly functionalities from one-way functions.
• Information-theoretically secure MPC for NC1 functionalities.

Both these protocols are secure against malicious (active) adversaries in the security with abort setting. Prior works could only handle a weaker corruption threshold (1/3) or required more rounds.

Based on joint works with Arka Rai Choudhuri, Aarushi Goel and Abhishek Jain.