Symbolic path cost analysis for side-channel detection

ABSTRACT

Side-channels in software are an increasingly significant threat to the confidentiality of private user information, and the static detection of such vulnerabilities is a key challenge in secure software development. In this paper, we introduce a new technique for scalable detection of side- channels in software. Given a program and a cost model for a side-channel (such as time or memory usage), we decompose the control flow graph of the program into nested branch and loop components, and compositionally assign a symbolic cost expression to each component. Symbolic cost expressions provide an over-approximation of all possible observable cost values that components can generate. Queries to a satisfiability solver on the difference between possible cost values of a component allow us to detect the presence of imbalanced paths (with respect to observable cost) through the control flow graph. When combined with taint analysis that identifies conditional statements that depend on secret information, our technique answers the following question: Does there exist a pair of paths in the program's control flow graph, differing only on branch conditions influenced by the secret, that differ in observable side-channel value by more than some given threshold? Additional optimization queries allow us to identify the minimal number of loop iterations necessary for the above to hold or the maximal cost difference between paths in the graph. We perform symbolic execution based feasibility analyses to eliminate control flow paths that are infeasible. We implemented our techniques in a prototype, and we demonstrate its favourable performance against state-of-the-art tools as well as its effectiveness and scalability on a set of sizable, realistic Java server-client and peer-to-peer applications.

References

1. {n. d.}. https://github.com/Apogee-Research/STAC/tree/master/Engagement_ Challenges. ({n. d.}).
2. {n. d.}. https://github.com/vlab-cs-ucsb/coco-channel. ({n. d.}).
3. {n. d.}. Space/Time Analysis for Cybersecurity (STAC). https://www.darpa.mil/ program/space-time-analysis-for-cybersecurity. ({n. d.}).
4. {n. d.}. Z3 API in Python. ({n. d.}). http://www.cs.tau.ac.il/~msagiv/courses/asv/ z3py/guide-examples.htm
5. Johan Agat. 2000. Transforming out timing leaks. In Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 40–53.
6. Saswat Anand, Corina Păsăreanu, and Willem Visser. 2007. JPF–SE: A symbolic execution extension to java pathfinder. Tools and Algorithms for the Construction and Analysis of Systems (2007), 134–138.
7. Timos Antopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei. 2017. Decomposition instead of self-composition for k-safety.
8. (2017).
9. Daniel Balasubramanian, Zhenkai Zhang, Dan McDermet, and Gabor Karsai. 2017. Janalyzer: A Static Analysis Tool for Java Bytecode. (08/2017 2017).
10. Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S Păsăreanu, and Tevfik Bultan. 2016. String analysis for side channels with segmented oracles. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM, 193–204.
11. Tegan Brennan, Seemanta Saha, and Tevfik Bultan. 2018. Symbolic Path Cost Analysis for Side-Channel Detection. In Software Engineering Companion (ICSEC), 2018 IEEE/ACM 40th International Conference on. IEEE.
12. David Brumley and Dan Boneh. 2005. Remote timing attacks are practical. Computer Networks 48, 5 (2005), 701–716.
13. Peter Chapman and David Evans. 2011. Automated black-box detection of side-channel vulnerabilities in web applications. In Proceedings of the 18th ACM conference on Computer and communications security. ACM, 263–274.
14. Jia Chen, Yu Feng, and Isil Dillig. 2017. Precise Detection of Side-Channel Vulnerabilities using Quantitative Cartesian Hoare Logic. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. ACM, 875–890.
15. Shuo Chen, Rui Wang, XiaoFeng Wang, and Kehuan Zhang. 2010. Side-channel leaks in web applications: A reality today, a challenge tomorrow. In Security and Privacy (SP), 2010 IEEE Symposium on. IEEE, 191–206.
16. Shigeru Chiba. 1998. JavassistâĂŤa reflection-based programming wizard for Java. In Proceedings of OOPSLAâĂŹ98 Workshop on Reflective Programming in C++ and Java, Vol. 174.
17. Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340.
18. Goran Doychev, Boris Köpf, Laurent Mauborgne, and Jan Reineke. 2015. Cacheaudit: A tool for the static analysis of cache side channels. ACM Transactions on Information and System Security (TISSEC) 18, 1 (2015), 4.
19. Jeffrey Friedman. 1972. Tempest: A signal problem. NSA Cryptologic Spectrum 35 (1972), 76.
20. Daniel Genkin, Itamar Pipman, and Eran Tromer. 2015. Get your hands off my laptop: Physical side-channel key-extraction attacks on PCs. Journal of Cryptographic Engineering 5, 2 (2015), 95–112.
21. Matthew S Hecht and Jeffrey D Ullman. 1972. Flow graph reducibility. In Proceedings of the fourth annual ACM symposium on Theory of computing. ACM, 238–250.
22. Daniel Hedin and David Sands. 2005. Timing aware information flow security for a javacard-like bytecode. Electronic Notes in Theoretical Computer Science 141, 1 (2005), 163–182.
23. Vincent Hindriksen. {n. d.}. How expensive is an operation on a CPU. ({n. d.}). https://streamhpc.com/blog/2012-07-16/ how-expensive-is-an-operation-on-a-cpu/
24. Ralf Hund, Carsten Willems, and Thorsten Holz. 2013. Practical timing side channel attacks against kernel space ASLR. In Security and Privacy (SP), 2013 IEEE Symposium on. IEEE, 191–205.
25. Marc Joye and Sung-Ming Yen. 2002. The Montgomery powering ladder. In CHES, Vol. 2. Springer, 291–302.
26. Paul C Kocher. 1996. Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In Annual International Cryptology Conference. Springer, 104–113.
27. Yau-Tsun Steven Li and Sharad Malik. 1995. Performance analysis of embedded software using implicit path enumeration. In ACM SIGPLAN Notices, Vol. 30. ACM, 88–98.
28. Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser, and Ruby B Lee. 2015. Lastlevel cache side-channel attacks are practical. In Security and Privacy (SP), 2015 IEEE Symposium on. IEEE, 605–622.
29. Edward S Lowry and Cleburne W Medlock. 1969. Object code optimization. Commun. ACM 12, 1 (1969), 13–22.
30. Luke Mather and Elisabeth Oswald. 2012. Quantifying Side-Channel Information Leakage from Web Applications. IACR Cryptology ePrint Archive 2012 (2012), 269.
31. Corina S Pasareanu, Quoc-Sang Phan, and Pasquale Malacaria. 2016. Multi-run side-channel analysis using Symbolic Execution and Max-SMT. In Computer Security Foundations Symposium (CSF), 2016 IEEE 29th. IEEE, 387–400.
32. Quoc-Sang Phan, Lucas Bang, Corina S Pasareanu, Pasquale Malacaria, and Tevfik Bultan. 2017. Synthesis of Adaptive Side-Channel Attacks. IACR Cryptology ePrint Archive 2017 (2017), 401.
33. Reese T Prosser. 1959. Applications of boolean matrices to the analysis of flow diagrams. In Papers presented at the December 1-3, 1959, eastern joint IRE-AIEEACM computer conference. ACM, 133–138.
34. Peter P Puschner and Anton V Schedl. 1997. Computing maximum task execution timesâĂŤa graph-based approach. Real-Time Systems 13, 1 (1997), 67–91.
35. Omer Tripp, Marco Pistoia, Stephen J Fink, Manu Sridharan, and Omri Weisman. 2009. TAJ: effective taint analysis of web applications. In ACM Sigplan Notices, Vol. 44. ACM, 87–97.
36. Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, et al. 2008.
37. The worst-case execution-time problemâĂŤoverview of methods and survey of tools. 7, 3 (2008), 36.

Index Terms

• Security and privacy

  • Software and application security

• Software and its engineering

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Automated static analysis