-
A Formal Model for Secure Multiparty Computation
Authors:
Amy Rathore,
Marina Blanton,
Marco Gaboardi,
Lukasz Ziarek
Abstract:
Although Secure Multiparty Computation (SMC) has seen considerable development in recent years, its use is challenging, resulting in complex code which obscures whether the security properties or correctness guarantees hold in practice. For this reason, several works have investigated the use of formal methods to provide guarantees for SMC systems. However, these approaches have been applied mostl…
▽ More
Although Secure Multiparty Computation (SMC) has seen considerable development in recent years, its use is challenging, resulting in complex code which obscures whether the security properties or correctness guarantees hold in practice. For this reason, several works have investigated the use of formal methods to provide guarantees for SMC systems. However, these approaches have been applied mostly to domain specific languages (DSL), neglecting general-purpose approaches. In this paper, we consider a formal model for an SMC system for annotated C programs. We choose C due to its popularity in the cryptographic community and being the only general-purpose language for which SMC compilers exist. Our formalization supports all key features of C -- including private-conditioned branching statements, mutable arrays (including out of bound array access), pointers to private data, etc. We use this formalization to characterize correctness and security properties of annotated C, with the latter being a form of non-interference on execution traces. We realize our formalism as an implementation in the PICCO SMC compiler and provide evaluation results on SMC programs written in C.
△ Less
Submitted 31 May, 2023;
originally announced June 2023.
-
TreeToaster: Towards an IVM-Optimized Compiler
Authors:
Darshana Balakrishnan,
Carl Nuessle,
Oliver Kennedy,
Lukasz Ziarek
Abstract:
A compiler's optimizer operates over abstract syntax trees (ASTs), continuously applying rewrite rules to replace subtrees of the AST with more efficient ones. Especially on large source repositories, even simply finding opportunities for a rewrite can be expensive, as optimizer traverses the AST naively. In this paper, we leverage the need to repeatedly find rewrites, and explore options for maki…
▽ More
A compiler's optimizer operates over abstract syntax trees (ASTs), continuously applying rewrite rules to replace subtrees of the AST with more efficient ones. Especially on large source repositories, even simply finding opportunities for a rewrite can be expensive, as optimizer traverses the AST naively. In this paper, we leverage the need to repeatedly find rewrites, and explore options for making the search faster through indexing and incremental view maintenance (IVM). Concretely, we consider bolt-on approaches that make use of embedded IVM systems like DBToaster, as well as two new approaches: Label-indexing and TreeToaster, an AST-specialized form of IVM. We integrate these approaches into an existing just-in-time data structure compiler and show experimentally that TreeToaster can significantly improve performance with minimal memory overheads.
△ Less
Submitted 2 April, 2021;
originally announced April 2021.
-
Understanding Bounding Functions in Safety-Critical UAV Software
Authors:
Xiaozhou Liang,
John Henry Burns,
Joseph Sanchez,
Karthik Dantu,
Lukasz Ziarek,
Yu David Liu
Abstract:
Unmanned Aerial Vehicles (UAVs) are an emerging computation platform known for their safety-critical need. In this paper, we conduct an empirical study on a widely used open-source UAV software framework, Paparazzi, with the goal of understanding the safety-critical concerns of UAV software from a bottom-up developer-in-the-field perspective. We set our focus on the use of Bounding Functions (BFs)…
▽ More
Unmanned Aerial Vehicles (UAVs) are an emerging computation platform known for their safety-critical need. In this paper, we conduct an empirical study on a widely used open-source UAV software framework, Paparazzi, with the goal of understanding the safety-critical concerns of UAV software from a bottom-up developer-in-the-field perspective. We set our focus on the use of Bounding Functions (BFs), the runtime checks injected by Paparazzi developers on the range of variables. Through an in-depth analysis on BFs in the Paparazzi autopilot software, we found a large number of them (109 instances) are used to bound safety-critical variables essential to the cyber-physical nature of the UAV, such as its thrust, its speed, and its sensor values. The novel contributions of this study are two fold. First, we take a static approach to classify all BF instances, presenting a novel datatype-based 5-category taxonomy with fine-grained insight on the role of BFs in ensuring the safety of UAV systems. Second, we dynamically evaluate the impact of the BF uses through a differential approach, establishing the UAV behavioral difference with and without BFs. The two-pronged static and dynamic approach together illuminates a rarely studied design space of safety-critical UAV software systems.
△ Less
Submitted 13 February, 2021;
originally announced February 2021.
-
Putting gradual types to work
Authors:
Bhargav Shivkumar,
Enrique Naudon,
Lukasz Ziarek
Abstract:
In this paper, we describe our experience incorporating gradual types in a statically typed functional language with Hindley-Milner style type inference. Where most gradually typed systems aim to improve static checking in a dynamically typed language, we approach it from the opposite perspective and promote dynamic checking in a statically typed language. Our approach provides a glimpse into how…
▽ More
In this paper, we describe our experience incorporating gradual types in a statically typed functional language with Hindley-Milner style type inference. Where most gradually typed systems aim to improve static checking in a dynamically typed language, we approach it from the opposite perspective and promote dynamic checking in a statically typed language. Our approach provides a glimpse into how languages like SML and OCaml might handle gradual ty**. We discuss our implementation and challenges faced -- specifically how gradual ty** rules apply to our representation of composite and recursive types. We review the various implementations that add dynamic ty** to a statically typed language in order to highlight the different ways of mixing static and dynamic ty** and examine possible inspirations while maintaining the gradual nature of our type system. This paper also discusses our motivation for adding gradual types to our language, and the practical benefits of doing so in our industrial setting.
△ Less
Submitted 28 January, 2021;
originally announced January 2021.
-
Just-in-Time Index Compilation
Authors:
Darshana Balakrishnan,
Lukasz Ziarek,
Oliver Kennedy
Abstract:
Creating or modifying a primary index is a time-consuming process, as the index typically needs to be rebuilt from scratch. In this paper, we explore a more graceful "just-in-time" approach to index reorganization, where small changes are dynamically applied in the background. To enable this type of reorganization, we formalize a composable organizational grammar, expressive enough to capture inst…
▽ More
Creating or modifying a primary index is a time-consuming process, as the index typically needs to be rebuilt from scratch. In this paper, we explore a more graceful "just-in-time" approach to index reorganization, where small changes are dynamically applied in the background. To enable this type of reorganization, we formalize a composable organizational grammar, expressive enough to capture instances of not only existing index structures, but arbitrary hybrids as well. We introduce an algebra of rewrite rules for such structures, and a framework for defining and optimizing policies for just-in-time rewriting. Our experimental analysis shows that the resulting index structure is flexible enough to adapt to a variety of performance goals, while also remaining competitive with existing structures like the C++ standard template library map.
△ Less
Submitted 22 January, 2019;
originally announced January 2019.
-
Embedded SML using the MLton compiler
Authors:
Jeffrey Murphy,
Bhargav Shivkumar,
Lukasz Ziarek
Abstract:
In this extended abstract we present our current work on leveraging Standard ML for develo** embedded and real-time systems. Specifically we detail our experiences in modifying MLton, a whole program, optimizing compiler for Standard ML, for use in such contexts. We focus primarily on the language runtime, re-working the threading subsystem and garbage collector, as well as necessary changes for…
▽ More
In this extended abstract we present our current work on leveraging Standard ML for develo** embedded and real-time systems. Specifically we detail our experiences in modifying MLton, a whole program, optimizing compiler for Standard ML, for use in such contexts. We focus primarily on the language runtime, re-working the threading subsystem and garbage collector, as well as necessary changes for integrating MLton generated programs into a light weight operating system kernel. We compare and contrast these changes to our previous work on extending MLton for multicore systems, which focused around acheiving scalability.
△ Less
Submitted 25 August, 2016;
originally announced August 2016.
-
Adding Real-time Capabilities to a SML Compiler
Authors:
Muyuan Li,
Daniel E McArdle,
Jeffrey C Murphy,
Bhargav Shivkumar,
Lukasz Ziarek
Abstract:
There has been much recent interest in adopting functional and reactive programming for use in real-time system design. Moving toward a more declarative methodology for develo** real-time systems purports to improve the fidelity of software. To study the benefits of functional and reactive programming for real-time systems, real-time aware functional compilers and language runtimes are required.…
▽ More
There has been much recent interest in adopting functional and reactive programming for use in real-time system design. Moving toward a more declarative methodology for develo** real-time systems purports to improve the fidelity of software. To study the benefits of functional and reactive programming for real-time systems, real-time aware functional compilers and language runtimes are required. In this paper we examine the necessary changes to a modern Standard ML compiler, MLton, to provide basic support for real-time execution. We detail our current progress in modifying MLton with a threading model that supports priorities, a chunked object model to support real-time garbage collection, and low level modification to execute on top of a real-time operating system. We present preliminary numbers and our work in progress prototype, which is able to boot ML programs compiled with MLton on x86 machines.
△ Less
Submitted 12 January, 2016;
originally announced January 2016.
-
BarQL: Collaborating Through Change
Authors:
Oliver Kennedy,
Lukasz Ziarek
Abstract:
Applications such as Google Docs, Office 365, and Dropbox show a growing trend towards incorporating multi-user live collaboration functionality into web applications. These collaborative applications share a need to efficiently express shared state, and a common strategy for doing so is a shared log abstraction. Extensive research efforts on log abstractions by the database, programming languages…
▽ More
Applications such as Google Docs, Office 365, and Dropbox show a growing trend towards incorporating multi-user live collaboration functionality into web applications. These collaborative applications share a need to efficiently express shared state, and a common strategy for doing so is a shared log abstraction. Extensive research efforts on log abstractions by the database, programming languages, and distributed systems communities have identified a variety of optimization techniques based on the algebraic properties of updates (i.e., pairwise commutativity, subsumption, and idempotence). Although these techniques have been applied to specific applications and use-cases, to the best of our knowledge, no attempt has been made to create a general framework for such optimizations in the context of a non-trivial update language. In this paper, we introduce mutation languages, a low-level framework for reasoning about the algebraic properties of state updates, or mutations. We define BarQL, a general purpose state-update language, and show how mutation languages allow us to reason about the algebraic properties of updates expressed in BarQ L .
△ Less
Submitted 18 March, 2013;
originally announced March 2013.
