MACS Project Meeting, December 2018
Date:
Friday, December 7, 2018
Location:
MIT, Star conference room (32D463) in the Stata Center at 32 Vassar St, Cambridge, MA
Schedule:
10 – 11:45 

11:45 – 12:15  Discussion of UC Analysis (Ran to moderate) 
12:15 – 1:45  Lunch (provided), and PI discussion in room G575 
1:45 – 3  
3 – 3:15  Break 
3:15 – 4:30 
Abstracts:
Sahil Tikale and Amin Mosayyebzadeh, Elastic Secure Marketplace for Trading Baremetal Servers
We describe our research efforts towards building a marketplace where different stakeholders from academia, research and industry can trade their baremetal 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 multicloud 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 baremetal 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 baremetal to workload ready in matter of minutes. It uses remotely mounted OS images making it possible to use baremetal servers like VMs that can be migrated with minimal loss of state.
Bolted is an effort to carve out a secure group of baremetal servers from a potentially nonsecure 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 nontrusting 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 opensource, nonproprietary package for managing cloud services and data centers. It is highly complex and consists of multiple interrelated 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 securitysensitive systems which are mostly noncryptographic, in nature, is one of the main contributions of this work. Our analysis is usercentric, 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 tradeoffs 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 coroutinebased execution model of the UC framework and the traditional procedural execution model of EasyCrypt, and we plan to develop a domainspecific 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 machinechecked 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 informationflowcontrol 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 privacyesque extension to our protocol in order to provide meaningful guarantees against inference attacks. Our protocol extends to other applications of keyvalue PIR protocols.
This work is implemented using JIFF, an easy to use generalpurpose 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 readonly 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 readonly 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, Appendonly 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 appendonly. Unfortunately, current transparency logs either provide smallsized (non)membership proofs or smallsized appendonly 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 appendonly authenticated dictionary (AAD). Our construction is the first to achieve (poly)logarithmic size for both proof types.
Alex Lombardi, Recent Progress on FiatShamir in the Plain Model
The FiatShamir heuristic provides a general template for transforming a publiccoin interactive proof into a noninteractive argument: the verifier in a (manyround) interactive proof is replaced by a hash function that the prover can query noninteractively. It is wellknown 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 FiatShamir 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 FiatShamir 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 tworound secure multiparty computation protocols in the honest majority setting:
 Secure MPC for P/poly functionalities from oneway functions.
 Informationtheoretically 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.