More Web Proxy on the site http://driver.im/

research-article

Abstract interpretation under speculative execution

Authors:

Chao WangAuthors Info & Claims

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 802 - 815

https://doi.org/10.1145/3314221.3314647

Published: 08 June 2019 Publication History

Abstract

Analyzing the behavior of a program running on a processor that supports speculative execution is crucial for applications such as execution time estimation and side channel detection. Unfortunately, existing static analysis techniques based on abstract interpretation do not model speculative execution since they focus on functional properties of a program while speculative execution does not change the functionality. To fill the gap, we propose a method to make abstract interpretation sound under speculative execution. There are two contributions. First, we introduce the notion of virtual control flow to augment instructions that may be speculatively executed and thus affect subsequent instructions. Second, to make the analysis efficient, we propose optimizations to handle merges and loops and to safely bound the speculative execution depth. We have implemented and evaluated the proposed method in a static cache analysis for execution time estimation and side channel detection. Our experiments show that the new method, while guaranteed to be sound under speculative execution, outperforms state-of-the-art abstract interpretation techniques that may be unsound.

Supplementary Material

WEBM File (p802-wu.webm)

Download
68.66 MB

References

[1]

2014. Intel®64 and IA-32 Architectures Optimization Reference Manual. https://botan.randombit.net/.

[2]

2018. LibTomCrypt: A Modular and Portable Cryptographic Toolkit. https://www.libtom.net/LibTomCrypt.

[3]

2018. OpenSSH. http://www.openssh.com/

[4]

2018. Tesla Motors: Linux. https://github.com/teslamotors/linux.

[5]

Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei. 2017. Decomposition instead of self-composition for proving the absence of timing channels. In ACM SIGPLAN Conference on Programming Language Design and Implementation. 362-375.

Digital Library

[6]

Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Pasareanu, and Tevfik Bultan. 2016. String analysis for side channels with segmented oracles. In ACM SIGSOFT Symposium on Foundations of Software Engineering. 193-204.

Digital Library

[7]

Gilles Barthe, Boris Köpf, Laurent Mauborgne, and Martín Ochoa. 2014. Leakage resilience against concurrent cache attacks. In International Conference on Principles of Security and Trust. 140-158.

[8]

Nathan L. Binkert, Bradford M. Beckmann, Gabriel Black, Steven K. Reinhardt, Ali G. Saidi, Arkaprava Basu, Joel Hestness, Derek Hower, Tushar Krishna, Somayeh Sardashti, Rathijit Sen, Korey Sewell, Muhammad Shoaib Bin Altaf, Nilay Vaish, Mark D. Hill, and David A. Wood. 2011. The GEM5 simulator. SIGARCH Computer Architecture News 39, 2 (2011), 1-7.

Digital Library

[9]

Tegan Brennan, Seemanta Saha, and Tevfik Bultan. 2018. Symbolic path cost analysis for side-channel detection. In International Conference on Software Engineering. 424-425.

Digital Library

[10]

Tevfik Bultan, Fang Yu, Muath Alkhalaf, and Abdulbaki Aydin. 2017. String Analysis for Software Verification and Security.

Digital Library

[11]

Jia Chen, Yu Feng, and Isil Dillig. 2017. Precise Detection of Side-Channel Vulnerabilities using Quantitative Cartesian Hoare Logic. In ACM SIGSAC Conference on Computer and Communications Security. 875-890.

Digital Library

[12]

Rapier Chris, Steven Michael, Bennett Benjamin, and Tasota Mike. 2018 (accessed March 1, 2019). High Performance SSH/SCP - HPN-SSH. https://www.psc.edu/hpn-ssh

[13]

Duc-Hiep Chu, Joxan Jaffar, and Rasool Maghareh. 2016. Precise cache timing analysis via symbolic execution. In IEEE Real-Time and Embedded Technology and Applications Symposium. 1-12.

[14]

Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 238-252.

Digital Library

[15]

Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Restraints Among Variables of a Program. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 84-96.

Digital Library

[16]

Goran Doychev, Dominik Feld, Boris Köpf, Laurent Mauborgne, and Jan Reineke. 2013. CacheAudit: A tool for the static analysis of cache side channels. In USENIX Security Symposium. 431-446.

Digital Library

[17]

Hassan Eldib, Chao Wang, and Patrick Schaumont. 2014. Formal Verification of Software Countermeasures against Side-Channel Attacks. ACM Trans. Softw. Eng. Methodol. 24, 2 (2014), 11:1-11:24.

Digital Library

[18]

Christian Ferdinand, Florian Martin, Reinhard Wilhelm, and Martin Alt. 1999. Cache behavior prediction by abstract interpretation. Science of Computer Programming 35, 2-3 (1999), 163-189.

Digital Library

[19]

Christian Ferdinand and Reinhard Wilhelm. 1998. On predicting data cache behavior for real-time systems. In ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems. 16-30.

Digital Library

[20]

Christian Ferdinand and Reinhard Wilhelm. 1999. Efficient and precise cache behavior prediction for real-time systems. Real-Time Systems 17, 2-3 (1999), 131-181.

Digital Library

[21]

Eliseu M. Chaves Filho and Edil S. Tavares Fernandes. 1997. The Effect of the Speculation Depth on the Performance of Superscalar Architectures. In International Euro-Par Conference on Parallel Processing. 1061-1065.

Digital Library

[22]

Qian Ge, Yuval Yarom, Tom Chothia, and Gernot Heiser. 2019. Time Protection: The Missing OS Abstraction. In Proceedings of the Fourteenth EuroSys Conference. 1:1-1:17.

Digital Library

[23]

Qian Ge, Yuval Yarom, David Cock, and Gernot Heiser. 2018. A survey of microarchitectural timing attacks and countermeasures on contemporary hardware. J. Cryptographic Engineering 8, 1 (2018), 1-27.

[24]

Shengjian Guo, Meng Wu, and Chao Wang. 2018. Adversarial symbolic execution for detecting concurrency-related cache timing leaks. In ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 377-388.

Digital Library

[25]

Jan Gustafsson, Adam Betts, Andreas Ermedahl, and Björn Lisper. 2010. The Mälardalen WCET Benchmarks - Past, Present and Future. In International Workshop on Worst-Case Execution Time Analysis. 137- 147.

[26]

Matthew R Guthaus, Jeffrey S Ringenberg, Dan Ernst, Todd M Austin, Trevor Mudge, and Richard B Brown. 2001. MiBench: A free, commercially representative embedded benchmark suite. In IEEE International Workshop on Workload Characterization. 3-14.

[27]

Daniel A Jiménez and Calvin Lin. 2001. Dynamic branch prediction with perceptrons. In IEEE International Symposium On High Performance Computer Architecture. 197-206.

Digital Library

[28]

Paul Kocher, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2018. Spectre Attacks: Exploiting Speculative Execution. ArXiv e-prints (Jan. 2018). arXiv:1801.01203

[29]

Boris Köpf, Laurent Mauborgne, and Martín Ochoa. 2012. Automatic quantification of cache side-channels. In International Conference on Computer Aided Verification. 564-580.

Digital Library

[30]

Markus Kusano and Chao Wang. 2016. Flow-Sensitive Composition of Thread-Modular Abstract Interpretation. In ACM SIGSOFT Symposium on Foundations of Software Engineering.

Digital Library

[31]

Markus Kusano and Chao Wang. 2017. Thread-modular static analysis for relaxed memory models. In ACM SIGSOFT Symposium on Foundations of Software Engineering. 337-348.

Digital Library

[32]

Chris Lattner and Vikram S. Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In IEEE / ACM International Symposium on Code Generation and Optimization. 75-88.

Digital Library

[33]

Xianfeng Li, Tulika Mitra, and Abhik Roychoudhury. 2003. Accurate timing analysis by modeling caches, speculation and their interaction. In ACM/IEEE Design Automation Conference. 466-471.

Digital Library

[34]

Xianfeng Li, Abhik Roychoudhury, and Tulika Mitra. 2006. Modeling out-of-order processors for WCET analysis. Real-Time Systems 34, 3 (2006), 195-227.

Digital Library

[35]

Yan Li, Vivy Suhendra, Yun Liang, Tulika Mitra, and Abhik Roychoudhury. 2009. Timing Analysis of Concurrent Programs Running on Shared Cache Multi-Cores. In IEEE Real-Time Systems Symposium. 57-67.

Digital Library

[36]

Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown. ArXiv e-prints (Jan. 2018). arXiv:1801.01207

[37]

Mingsong Lv, Wang Yi, Nan Guan, and Ge Yu. 2010. Combining abstract interpretation with model checking for timing analysis of multicore software. In IEEE Real-Time Systems Symposium. 339-349.

Digital Library

[38]

Laurent Mauborgne and Xavier Rival. 2005. Trace Partitioning in Abstract Interpretation Based Static Analyzers. In European Symposium on Programming Languages and Systems. 5-20.

Digital Library

[39]

Ravindra Metta, Martin Becker, Prasad Bokil, Samarjit Chakraborty, and R Venkatesh. 2016. TIC: a scalable model checking based approach to WCET estimation. In ACM SIGPLAN Notices, Vol. 51. ACM, 72-81.

Digital Library

[40]

Antoine Miné. 2006. The octagon abstract domain. Higher-order and symbolic computation 19, 1 (2006), 31-100.

Digital Library

[41]

Tulika Mitra, Jürgen Teich, and Lothar Thiele. 2018. Time-Critical Systems Design: A Survey. IEEE Design & Test 35, 2 (2018), 8-26.

[42]

F Nielson, Riis H Nielson, and CL Hankin. 1999. Principles of Program Analysis. (1999).

Digital Library

[43]

Corina S. Pasareanu, Quoc-Sang Phan, and Pasquale Malacaria. 2016. Multi-run Side-Channel Analysis Using Symbolic Execution and Max-SMT. In IEEE Computer Security Foundations Symposium. 387-400.

[44]

Quoc-Sang Phan, Lucas Bang, Corina S. Pasareanu, Pasquale Malacaria, and Tevfik Bultan. 2017. Synthesis of Adaptive Side-Channel Attacks. In IEEE Computer Security Foundations Symposium. 328-342.

[45]

Jim Pierce and Trevor N. Mudge. 1994. The Effect of Speculative Execution on Cache Performance. In International Symposium on Parallel Processing. 172-179.

Digital Library

[46]

Jörn Schneider. 1998. Statische pipeline-analyse für echtzeitsysteme. Dipl. thesis, Univ. Saarland, Saarbruecken, Germany (1998).

[47]

Jörn Schneider and Christian Ferdinand. 1999. Pipeline behavior prediction for superscalar processors by abstract interpretation. In ACM SIGPLAN Notices, Vol. 34. 35-44.

Digital Library

[48]

Rathijit Sen and Y. N. Srikant. 2007. WCET estimation for executables in the presence of data caches. In ACM/IEEE International conference on Embedded Software. 203-212.

Digital Library

[49]

Marcelo Sousa and Isil Dillig. 2016. Cartesian hoare logic for verifying k-safety properties. In ACM SIGPLAN Conference on Programming Language Design and Implementation. 57-69.

Digital Library

[50]

Chungha Sung, Markus Kusano, and Chao Wang. 2017. Modular verification of interrupt-driven software. In IEEE/ACM International Conference On Automated Software Engineering. 206-216.

Digital Library

[51]

Chungha Sung, Brandon Paulsen, and Chao Wang. 2018. CANAL: a cache timing analysis framework via LLVM transformation. In IEEE/ACM International Conference On Automated Software Engineering. 904-907.

Digital Library

[52]

Henrik Theiling, Christian Ferdinand, and Reinhard Wilhelm. 2000. Fast and precise WCET prediction by separated cache and path analyses. Real-Time Systems 18, 2 (2000), 157-179.

Digital Library

[53]

R. M. Tomasulo. 1967. An Efficient Algorithm for Exploiting Multiple Arithmetic Units. IBM Journal of Research and Development 11, 1 (Jan 1967), 25-33.

Digital Library

[54]

Valentin Touzeau, Claire Maiza, David Monniaux, and Jan Reineke. 2017. Ascertaining uncertainty for efficient exact cache analysis. In International Conference on Computer Aided Verification. 22-40.

[55]

Jo Van Bulck, Marina Minkin, Ofir Weisse, Daniel Genkin, Baris Kasikci, Frank Piessens, Mark Silberstein, Thomas F. Wenisch, Yuval Yarom, and Raoul Strackx. 2018. Foreshadow: Extracting the Keys to the Intel SGX Kingdom with Transient Out-of-Order Execution. In USENIX Security Symposium.

Digital Library

[56]

Lucian N Vintan and Mihaela Iridon. 1999. Towards a high performance neural branch predictor. In International Joint Conference on Neural Networks. 868-873.

[57]

Reinhard Wilhelm, Sebastian Altmeyer, Claire Burguière, Daniel Grund, Jörg Herter, Jan Reineke, BjörnWachter, and Stephan Wilhelm. 2010. Static timing analysis for hard real-time systems. In International Workshop on Verification, Model Checking, and Abstract Interpretation. 3-22.

Digital Library

[58]

Meng Wu, Shengjian Guo, Patrick Schaumont, and Chao Wang. 2018. Eliminating timing side-channel leaks using program repair. In International Symposium on Software Testing and Analysis. 15-26.

Digital Library

[59]

Tse-Yu Yeh and Yale N Patt. 1991. Two-level adaptive training branch prediction. In IEEE/ACM International Symposium on Microarchitecture. 51-61.

Digital Library

[60]

Jun Zhang, Pengfei Gao, Fu Song, and Chao Wang. 2018. SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks. In International Conference on Computer Aided Verification. 157-177.

Cited By

Tan QYang YBourgeat TMalik SYan MEeckhout LSmaragdakis GLiang KSampson AKim MRossbach C(2025)RTL Verification for Secure Speculation Using Contract Shadow LogicProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3669940.3707243(970-986)Online publication date: 30-Mar-2025
https://dl.acm.org/doi/10.1145/3669940.3707243
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
Marinaro TBuiras PLindner AGuanciale RNemati HQuek TGao DZhou JCardenas A(2024)Beyond Over-Protection: A Targeted Approach to Spectre Mitigation and Performance OptimizationProceedings of the 19th ACM Asia Conference on Computer and Communications Security10.1145/3634737.3637651(203-216)Online publication date: 1-Jul-2024
https://dl.acm.org/doi/10.1145/3634737.3637651
Show More Cited By

Index Terms

Abstract interpretation under speculative execution
1. Security and privacy
  1. Cryptography
    1. Cryptanalysis and other attacks
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software notations and tools
    1. Compilers

Recommendations

Using Predicated Execution to Improve the Performance of a Dynamically Scheduled Machine with Speculative Execution

Conditional branches incur a severe performance penalty in wide-issue, deeply pipelined processors. Speculative execution(1, 2) and predicated execution(3---9) are two mechanisms that have been proposed for reducing this penalty. Speculative execution ...
Three Architectural Models for Compiler-Controlled Speculative Execution

To effectively exploit instruction level parallelism, the compiler must move instructions across branches. When an instruction is moved above a branch that it is control dependent on, it is considered to be speculatively executed since it is executed ...
Statically Safe Speculative Execution for Real-Time Systems

Deterministic worst-case execution for satisfying hard-real-time constraints, and speculative execution with rollback for improving average-case throughput, appear to lie on opposite ends of a spectrum of performance requirements and strategies. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2019

1162 pages

ISBN:9781450367127

DOI:10.1145/3314221

General Chair:
Kathryn S. McKinley
Google, USA
,
Program Chair:
Kathleen Fisher
Tufts University, USA

Copyright © 2019 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 June 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '19

Sponsor:

SIGPLAN

PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 22 - 26, 2019

AZ, Phoenix, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
464
Total Downloads

Downloads (Last 12 months)39
Downloads (Last 6 weeks)6

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Tan QYang YBourgeat TMalik SYan MEeckhout LSmaragdakis GLiang KSampson AKim MRossbach C(2025)RTL Verification for Secure Speculation Using Contract Shadow LogicProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3669940.3707243(970-986)Online publication date: 30-Mar-2025
https://dl.acm.org/doi/10.1145/3669940.3707243
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
Marinaro TBuiras PLindner AGuanciale RNemati HQuek TGao DZhou JCardenas A(2024)Beyond Over-Protection: A Targeted Approach to Spectre Mitigation and Performance OptimizationProceedings of the 19th ACM Asia Conference on Computer and Communications Security10.1145/3634737.3637651(203-216)Online publication date: 1-Jul-2024
https://dl.acm.org/doi/10.1145/3634737.3637651
Hu QDing YLiu CLi KLi KZomaya A(2024)CBANA: A Lightweight, Efficient, and Flexible Cache Behavior Analysis FrameworkIEEE Transactions on Computers10.1109/TC.2024.341674773:9(2262-2274)Online publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1109/TC.2024.3416747
Zhang ZBarthe GChuengsatiansup CSchwabe PYarom YCalandrino JTroncoso C(2023)Ultimate SLHProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620636(7125-7142)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620636
Li YWang JWang CJust RFraser G(2023)Systematic Testing of the Data-Poisoning Robustness of KNNProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598129(1207-1218)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598129
Yang YBourgeat TLau SYan MSolihin YHeinrich M(2023)Pensieve: Microarchitectural Modeling for Security EvaluationProceedings of the 50th Annual International Symposium on Computer Architecture10.1145/3579371.3589094(1-15)Online publication date: 17-Jun-2023
https://dl.acm.org/doi/10.1145/3579371.3589094
Jang HShin Y(2023)MicroCFI: Microarchitecture-Level Control-Flow Restrictions for Spectre MitigationIEEE Access10.1109/ACCESS.2023.334068011(138699-138711)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3340680
Llorente-Vazquez OSantos-Grueiro IBringas P(2023)When Memory Corruption Met Concurrency: Vulnerabilities in Concurrent ProgramsIEEE Access10.1109/ACCESS.2023.327283311(44725-44740)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3272833
Li YWang JWang C(2023)Certifying the Fairness of KNN in the Presence of Dataset BiasComputer Aided Verification10.1007/978-3-031-37703-7_16(335-357)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37703-7_16
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten