DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2019.11

Eventually Sound Points-To Analysis with Specifications

Authors: Osbert Bastani, Rahul Sharma, Lazaro Clapp, Saswat Anand, and Alex Aiken

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract

Static analyses make the increasingly tenuous assumption that all source code is available for analysis; for example, large libraries often call into native code that cannot be analyzed. We propose a points-to analysis that initially makes optimistic assumptions about missing code, and then inserts runtime checks that report counterexamples to these assumptions that occur during execution. Our approach guarantees eventual soundness, which combines two guarantees: (i) the runtime checks are guaranteed to catch the first counterexample that occurs during any execution, in which case execution can be terminated to prevent harm, and (ii) only finitely many counterexamples ever occur, implying that the static analysis eventually becomes statically sound with respect to all remaining executions. We implement Optix, an eventually sound points-to analysis for Android apps, where the Android framework is missing. We show that the runtime checks added by Optix incur low overhead on real programs, and demonstrate how Optix improves a client information flow analysis for detecting Android malware.

Cite as

Osbert Bastani, Rahul Sharma, Lazaro Clapp, Saswat Anand, and Alex Aiken. Eventually Sound Points-To Analysis with Specifications. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 11:1-11:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bastani_et_al:LIPIcs.ECOOP.2019.11,
  author =	{Bastani, Osbert and Sharma, Rahul and Clapp, Lazaro and Anand, Saswat and Aiken, Alex},
  title =	{{Eventually Sound Points-To Analysis with Specifications}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{11:1--11:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.11},
  URN =		{urn:nbn:de:0030-drops-108038},
  doi =		{10.4230/LIPIcs.ECOOP.2019.11},
  annote =	{Keywords: specification inference, static points-to analysis, runtime monitoring}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSTTCS.2011.6

A Domain-Specific Language for Computing on Encrypted Data (Invited Talk)

Authors: Alex Bain, John Mitchell, Rahul Sharma, Deian Stefan, and Joe Zimmerman

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract

In cloud computing, a client may request computation on confidential data that is sent to untrusted servers. While homomorphic encryption and secure multiparty computation provide building blocks for secure computation, software must be properly structured to preserve confidentiality. Using a general definition of secure execution platform, we propose a single Haskell-based domain-specific language for cryptographic cloud computing and prove correctness and confidentiality for two representative and distinctly different implementations of the same programming language. The secret sharing execution platform provides information-theoretic security against colluding servers. The homomorphic encryption execution platform requires only one server, but has limited efficiency, and provides secrecy against a computationally-bounded adversary. Experiments with our implementation suggest promising computational feasibility, as cryptography improves, and show how code can be developed uniformly for a variety of secure cloud platforms, without explicitly programming separate clients and servers.

Cite as

Alex Bain, John Mitchell, Rahul Sharma, Deian Stefan, and Joe Zimmerman. A Domain-Specific Language for Computing on Encrypted Data (Invited Talk). In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 6-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bain_et_al:LIPIcs.FSTTCS.2011.6,
  author =	{Bain, Alex and Mitchell, John and Sharma, Rahul and Stefan, Deian and Zimmerman, Joe},
  title =	{{A Domain-Specific Language for Computing on Encrypted Data}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{6--24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.6},
  URN =		{urn:nbn:de:0030-drops-33604},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.6},
  annote =	{Keywords: Domain-Specific Language, Secret Sharing, Homomorphic Encryption}
}

Search Results

Documents authored by Sharma, Rahul

Eventually Sound Points-To Analysis with Specifications

Abstract

Cite as

A Domain-Specific Language for Computing on Encrypted Data (Invited Talk)

Abstract

Cite as

Thanks for your feedback!

Could not send message