research-article

Public Access

String analysis for side channels with segmented oracles

Authors:

Abdulbaki Aydin,

Quoc-Sang Phan,

Corina S. Păsăreanu,

Tevfik BultanAuthors Info & Claims

FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

Pages 193 - 204

https://doi.org/10.1145/2950290.2950362

Published: 01 November 2016 Publication History

Abstract

We present an automated approach for detecting and quantifying side channels in Java programs, which uses symbolic execution, string analysis and model counting to compute information leakage for a single run of a program. We further extend this approach to compute information leakage for multiple runs for a type of side channels called segmented oracles, where the attacker is able to explore each segment of a secret (for example each character of a password) independently. We present an efficient technique for segmented oracles that computes information leakage for multiple runs using only the path constraints generated from a single run symbolic execution. Our implementation uses the symbolic execution tool Symbolic PathFinder (SPF), SMT solver Z3, and two model counting constraint solvers LattE and ABC. Although LattE has been used before for analyzing numeric constraints, in this paper, we present an approach for using LattE for analyzing string constraints. We also extend the string constraint solver ABC for analysis of both numeric and string constraints, and we integrate ABC in SPF, enabling quantitative symbolic string analysis.

References

[1]

Omega. http://www.cs.umd.edu/projects/omega/.

[2]

Xbox 360 timing attack. http://beta.ivc.no/wiki/ index.php/Xbox 360 Timing Attack, 2007.

[3]

A few important facts regarding oauth security. http://oauthlib.readthedocs.io/en/latest/oauth1/ security.html, 2012.

[4]

Oauth protocol hmac byte value calculation timing disclosure weakness. https://osvdb.info/OSVDB-97562, 2013.

[5]

P. A. Abdulla, M. F. Atig, Y. Chen, L. Hol´ık, A. Rezine, P. Rümmer, and J. Stenman. String constraints for verification. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV), pages 150–166, 2014.

Digital Library

[6]

A. Aydin, L. Bang, and T. Bultan. Automata-based model counting for string constraints. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV), pages 255–272, 2015.

[7]

M. Backes, B. Kopf, and A. Rybalchenko. Automatic Discovery and Quantification of Information Leaks. In Proceedings of the 2009 30th IEEE Symposium on Security and Privacy, SP ’09, pages 141–153, Washington, DC, USA, 2009. IEEE Computer Society.

Digital Library

[8]

C. Bartzis and T. Bultan. Efficient symbolic representations for arithmetic constraints in verification. Int. J. Found. Comput. Sci., 14(4):605–624, 2003.

[9]

D. Brumley and D. Boneh. Remote Timing Attacks Are Practical. In Proceedings of the 12th Conference on USENIX Security Symposium - Volume 12, SSYM’03, pages 1–1, Berkeley, CA, USA, 2003. USENIX Association.

Digital Library

[10]

S. Chen, R. Wang, X. Wang, and K. Zhang. Side-channel leaks in web applications: A reality today, a challenge tomorrow. In Proceedings of the 2010 IEEE Symposium on Security and Privacy, SP ’10, pages 191–206, Washington, DC, USA, 2010. IEEE Computer Society.

Digital Library

[11]

T. Chothia, Y. Kawamoto, and C. Novakovic. Leakwatch: Estimating information leakage from java programs. In M. Kutylowski and J. Vaidya, editors, Computer Security - ESORICS 2014 - 19th European Symposium on Research in Computer Security, Wroclaw, Poland, September 7-11, 2014. Proceedings, Part II, volume 8713 of Lecture Notes in Computer Science, pages 219–236. Springer, 2014.

Digital Library

[12]

D. Clark, S. Hunt, and P. Malacaria. A static analysis for quantifying information flow in a simple imperative language. J. Comput. Secur., 15(3):321–371, Aug. 2007.

Digital Library

[13]

J. S. Daniel Mayer. Time trial: Racing towards practical remote timing attacks. https://www.nccgroup.trust/globalassets/ our-research/us/whitepapers/TimeTrial.pdf, 2014.

[14]

G. Doychev, B. Köpf, L. Mauborgne, and J. Reineke. Cacheaudit: A tool for the static analysis of cache side channels. ACM Trans. Inf. Syst. Secur., 18(1):4, 2015.

Digital Library

[15]

A. Filieri, C. S. Pasareanu, and W. Visser. Reliability analysis in symbolic pathfinder. In Proceedings of the 35th International Conference on Software Engineering (ICSE), pages 622–631, 2013.

Digital Library

[16]

A. Filieri, C. S. Păsăreanu, and W. Visser. Reliability analysis in symbolic pathfinder. In Proceedings of the 2013 International Conference on Software Engineering, ICSE ’13, pages 622–631, Piscataway, NJ, USA, 2013. IEEE Press.

Digital Library

[17]

V. Ganesh, M. Minnes, A. Solar-Lezama, and M. C. Rinard. Word equations with length constraints: What’s decidable? In Proceedings of the 8th International Haifa Verification Conference (HVC), pages 209–226, 2012.

Digital Library

[18]

C. Hale. A lesson in timing attacks (or, donˆ a ˘ A´ Zt use messagedigest.isequals). https://codahale.com/a-lesson-in-timing-attacks/, 2009.

[19]

J. Heusser and P. Malacaria. Quantifying information leaks in software. In Proceedings of the 26th Annual Computer Security Applications Conference, ACSAC ’10, pages 261–269, New York, NY, USA, 2010. ACM.

Digital Library

[20]

P. Hooimeijer and W. Weimer. A decision procedure for subset constraints over regular languages. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 188–198, 2009.

Digital Library

[21]

P. Hooimeijer and W. Weimer. Solving string constraints lazily. In Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 377–386, 2010.

Digital Library

[22]

M. Joye. Basics of side-channel analysis. In Cryptographic Engineering, chapter 13, pages 367–382. 2009.

[23]

S. Kausler and E. Sherman. Evaluation of string constraint solvers in the context of symbolic execution. In Proceedings of the 29th ACM/IEEE International Conference on Automated software engineering (ASE), pages 259–270, 2014.

Digital Library

[24]

J. Kelsey. Compression and information leakage of plaintext. In Fast Software Encryption, 9th International Workshop, FSE 2002, Leuven, Belgium, February 4-6, 2002, Revised Papers, pages 263–276, 2002.

Digital Library

[25]

A. Kiezun, V. Ganesh, P. J. Guo, P. Hooimeijer, and M. D. Ernst. Hampi: a solver for string constraints. In Proceedings of the 18th International Symposium on Software Testing and Analysis (ISSTA), pages 105–116, 2009.

Digital Library

[26]

J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385–394, July 1976.

Digital Library

[27]

V. Klebanov, N. Manthey, and C. Muise. SAT-Based Analysis and Quantification of Information Flow in Programs. In Quantitative Evaluation of Systems, volume 8054 of Lecture Notes in Computer Science, pages 177–192. Springer Berlin Heidelberg, 2013.

Digital Library

[28]

P. C. Kocher. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology, CRYPTO ’96, pages 104–113, London, UK, UK, 1996. Springer-Verlag.

Digital Library

[29]

B. Köpf and D. A. Basin. An information-theoretic model for adaptive side-channel attacks. In P. Ning, S. D. C. di Vimercati, and P. F. Syverson, editors, Proceedings of the 2007 ACM Conference on Computer and Communications Security, CCS 2007, Alexandria, Virginia, USA, October 28-31, 2007, pages 286–296. ACM, 2007.

Digital Library

[30]

N. Lawson. Side-channel attacks on cryptographic software. IEEE Security and Privacy, 7(6):65–68, Nov. 2009.

Digital Library

[31]

N. Lawson. Timing attack in google keyczar library. https://rdist.root.org/2009/05/28/ timing-attack-in-google-keyczar-library/, 2009.

[32]

N. Lawson. Optimized memcmp leaks useful timing differences. https://rdist.root.org/2010/08/05/ optimized-memcmp-leaks-useful-timing-differences/, 2010.

[33]

G. Li and I. Ghosh. PASS: string solving with parameterized array and interval automaton. In Proceedings of the 9th International Haifa Verification Conference (HVC), pages 15–31, 2013.

[34]

T. Liang, A. Reynolds, C. Tinelli, C. Barrett, and M. Deters. A DPLL(T) theory solver for a theory of strings and regular expressions. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV), pages 646–662, 2014.

Digital Library

[35]

J. A. D. Loera, R. Hemmecke, J. Tauzer, and R. Yoshida. Effective lattice point counting in rational convex polytopes. Journal of Symbolic Computation, 38(4):1273 – 1302, 2004. Symbolic Computation in Algebra and Geometry.

[36]

L. Luu, S. Shinde, P. Saxena, and B. Demsky. A model counter for constraints over unbounded strings. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), page 57, 2014.

Digital Library

[37]

P. Mardziel, M. S. Alvim, M. W. Hicks, and M. R. Clarkson. Quantifying information flow for dynamic secrets. In 2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, May 18-21, 2014, pages 540–555, 2014.

Digital Library

[38]

S. McCamant and M. D. Ernst. Quantitative information flow as network flow capacity. In Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, PLDI ’08, pages 193–205, New York, NY, USA, 2008. ACM.

Digital Library

[39]

Microsoft Inc. Z3 SMT Solver. http://z3.codeplex.com.

[40]

T. Nelson. Widespread timing vulnerabilities in openid implementations. http://lists.openid.net/pipermail/ openid-security/2010-July/001156.html, 2010.

[41]

Q.-S. Phan and P. Malacaria. Abstract Model Counting: A Novel Approach for Quantification of Information Leaks. In Proceedings of the 9th ACM Symposium on Information, Computer and Communications Security, ASIA CCS ’14, pages 283–292, New York, NY, USA, 2014. ACM.

Digital Library

[42]

Q.-S. Phan, P. Malacaria, C. S. Păsăreanu, and M. d’Amorim. Quantifying Information Leaks Using Reliability Analysis. In Proceedings of the 2014 International SPIN Symposium on Model Checking of Software, SPIN 2014, pages 105–108, New York, NY, USA, 2014. ACM.

Digital Library

[43]

Q.-S. Phan, P. Malacaria, O. Tkachuk, and C. S. Păsăreanu. Symbolic Quantitative Information Flow. SIGSOFT Softw. Eng. Notes, 37(6):1–5, Nov. 2012.

Digital Library

[44]

C. S. Păsăreanu, Q.-S. Phan, and P. Malacaria. Multi-run side-channel analysis using Symbolic Execution and Max-SMT. In Proceedings of the 2016 IEEE 29th Computer Security Foundations Symposium, CSF ’16, Washington, DC, USA, 2016. IEEE Computer Society.

[45]

C. S. Păsăreanu, W. Visser, D. Bushnell, J. Geldenhuys, P. Mehlitz, and N. Rungta. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering, pages 1–35, 2013.

[46]

J. Rizzo and T. Duong. The crime attack. Ekoparty Security Conference, 2012.

[47]

P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song. A symbolic execution framework for javascript. In Proceedings of the 31st IEEE Symposium on Security and Privacy, 2010.

Digital Library

[48]

M. Trinh, D. Chu, and J. Jaffar. S3: A symbolic string solver for vulnerability detection in web applications. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 1232–1243, 2014.

Digital Library

[49]

F. Weimer. Defeating memory comparison timing oracles. https: //access.redhat.com/blogs/766093/posts/878863/, 2014.

[50]

F. Yu, M. Alkhalaf, and T. Bultan. Stranger: An automata-based string analysis tool for php. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 154–157, 2010.

Digital Library

[51]

F. Yu, M. Alkhalaf, T. Bultan, and O. H. Ibarra. Automata-based symbolic string analysis for vulnerability detection. Formal Methods in System Design, 44(1):44–70, 2014.

Digital Library

[52]

F. Yu, T. Bultan, M. Cova, and O. H. Ibarra. Symbolic string verification: An automata-based approach. In Proceedings of the 15th International SPIN Workshop on Model Checking Software (SPIN), pages 306–324, 2008.

Digital Library

[53]

Y. Zheng, X. Zhang, and V. Ganesh. Z3-str: A z3-based string solver for web application analysis. In Proceedings of the 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE), pages 114–124, 2013.

Digital Library

[54]

J. Ziv and A. Lempel. A universal algorithm for sequential data compression. IEEE Transactions on Information Theory, 23(3):337–343, May 1977.

Digital Library

Cited By

Ruan HNoller YTizpaz-Niari SChattopadhyay SRoychoudhury A(2024)Timing Side-Channel Mitigation via Automated Program RepairACM Transactions on Software Engineering and Methodology10.1145/367816933:8(1-27)Online publication date: 16-Jul-2024
https://dl.acm.org/doi/10.1145/3678169
Meel KChakraborty SMathur U(2024)A faster FPRAS for #NFAProceedings of the ACM on Management of Data10.1145/36516132:2(1-22)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3651613
Cai LSong FChen T(2024)Towards Efficient Verification of Constant-Time Cryptographic ImplementationsProceedings of the ACM on Software Engineering10.1145/36437721:FSE(1019-1042)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643772
Show More Cited By

Index Terms

String analysis for side channels with segmented oracles
1. Security and privacy
  1. Formal methods and theory of security
    1. Logic and verification
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

Memory Modeling-Based Automatic Test Data Generation for String-Manipulating Programs
APSEC '12: Proceedings of the 2012 19th Asia-Pacific Software Engineering Conference - Volume 02

String is a fundamental data type in C programming language, and is accessed through character pointer. Programs that manipulate string variables often use a set of string library functions. When generating test data for a path in a function with string ...
Lightweight string reasoning in model finding

Models play a key role in assuring software quality in the model-driven approach. Precise models usually require the definition of well-formedness rules to specify constraints that cannot be expressed graphically. The Object Constraint Language (OCL) is ...
Solving String Constraints with Lengths by Stabilization

We present a new algorithm for solving string constraints. The algorithm builds upon a recent method for solving word equations and regular constraints that interprets string variables as languages rather than strings and, consequently, mitigates the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

November 2016

1156 pages

ISBN:9781450342186

DOI:10.1145/2950290

General Chair:
Thomas Zimmermann
Microsoft Research, USA
,
Program Chairs:
Jane Cleland-Huang
University of Notre Dame, USA
,
Zhendong Su
University of California at Davis, USA

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

FSE'16

Sponsor:

SIGSOFT

FSE'16: 24nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering

November 13 - 18, 2016

WA, Seattle, USA

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

53
Total Citations
View Citations
673
Total Downloads

Downloads (Last 12 months)101
Downloads (Last 6 weeks)8

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ruan HNoller YTizpaz-Niari SChattopadhyay SRoychoudhury A(2024)Timing Side-Channel Mitigation via Automated Program RepairACM Transactions on Software Engineering and Methodology10.1145/367816933:8(1-27)Online publication date: 16-Jul-2024
https://dl.acm.org/doi/10.1145/3678169
Meel KChakraborty SMathur U(2024)A faster FPRAS for #NFAProceedings of the ACM on Management of Data10.1145/36516132:2(1-22)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3651613
Cai LSong FChen T(2024)Towards Efficient Verification of Constant-Time Cryptographic ImplementationsProceedings of the ACM on Software Engineering10.1145/36437721:FSE(1019-1042)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643772
Gao PSong FChen T(2024)Compositional Verification of First-Order Masking Countermeasures against Power Side-Channel AttacksACM Transactions on Software Engineering and Methodology10.1145/363570733:3(1-38)Online publication date: 14-Mar-2024
https://dl.acm.org/doi/10.1145/3635707
Saha SGhentiyala SLu SBang LBultan T(2023)Obtaining Information Leakage Bounds via Approximate Model CountingProceedings of the ACM on Programming Languages10.1145/35912817:PLDI(1488-1509)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591281
Schwarzl MBorrello PSaileshwar GMüller HSchwarz MGruss D(2023)Practical Timing Side-Channel Attacks on Memory Compression2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179297(1186-1203)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179297
Eiers WSankaran GLi AO'Mahony EPrince BBultan TDwyer MDamian DZeller A(2022)Quantifying permissiveness of access control policiesProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510233(1805-1817)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510233
Saha SDowning MBrennan TBultan TDwyer MDamian DZeller A(2022)PReachProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510227(1706-1717)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510227
Sun WYan ZXu XDing WGao L(2022)Software Side Channel Vulnerability Detection Based on Similarity Calculation and Deep Learning2022 IEEE International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom)10.1109/TrustCom56396.2022.00112(800-809)Online publication date: Dec-2022
https://doi.org/10.1109/TrustCom56396.2022.00112
Golia PJuba BMeel K(2022)A Scalable Shannon Entropy EstimatorComputer Aided Verification10.1007/978-3-031-13185-1_18(363-384)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_18
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents