TY - GEN
T1 - AutoCC
T2 - 56th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2023
AU - Orenes-Vera, Marcelo
AU - Yun, Hyunsung
AU - Wistoff, Nils
AU - Heiser, Gernot
AU - Benini, Luca
AU - Wentzlaff, David
AU - Martonosi, Margaret
N1 - Publisher Copyright:
© 2023 Owner/Author.
PY - 2023/10/28
Y1 - 2023/10/28
N2 - Covert channels enable information leakage between security domains that should be isolated by observing execution differences in shared hardware. These channels can appear in any stateful shared resource, including caches, predictors, and accelerators. Previous works have identified many vulnerable components, demonstrating and defending against attacks via reverse engineering. However, this approach requires much human effort and reasoning. With the Cambrian explosion of specialized hardware, it is becoming increasingly difficult to identify all vulnerabilities manually. To tackle this challenge, we propose AutoCC, a methodology that leverages formal property verification (FPV) to automatically discover covert channels in hardware that is shared between processes. AutoCC operates at the register-transfer level (RTL) to exhaustively examine any machine state left by a process after a context switch that creates an execution difference. Upon finding such a difference, AutoCC provides a precise execution trace showing how the information was encoded into the machine state and recovered. Leveraging AutoCC's flow to generate FPV testbenches that apply our methodology, we evaluated it on four open-source hardware projects, including two RISC-V cores and two accelerators. Without hand-written code or directed tests, AutoCC uncovered known covert channels (within minutes instead of many hours of test-driven emulations) and unknown ones. Although AutoCC is primarily intended to find covert channels, our evaluation has also found RTL bugs, demonstrating that AutoCC is an effective tool to test both the security and reliability of hardware designs.
AB - Covert channels enable information leakage between security domains that should be isolated by observing execution differences in shared hardware. These channels can appear in any stateful shared resource, including caches, predictors, and accelerators. Previous works have identified many vulnerable components, demonstrating and defending against attacks via reverse engineering. However, this approach requires much human effort and reasoning. With the Cambrian explosion of specialized hardware, it is becoming increasingly difficult to identify all vulnerabilities manually. To tackle this challenge, we propose AutoCC, a methodology that leverages formal property verification (FPV) to automatically discover covert channels in hardware that is shared between processes. AutoCC operates at the register-transfer level (RTL) to exhaustively examine any machine state left by a process after a context switch that creates an execution difference. Upon finding such a difference, AutoCC provides a precise execution trace showing how the information was encoded into the machine state and recovered. Leveraging AutoCC's flow to generate FPV testbenches that apply our methodology, we evaluated it on four open-source hardware projects, including two RISC-V cores and two accelerators. Without hand-written code or directed tests, AutoCC uncovered known covert channels (within minutes instead of many hours of test-driven emulations) and unknown ones. Although AutoCC is primarily intended to find covert channels, our evaluation has also found RTL bugs, demonstrating that AutoCC is an effective tool to test both the security and reliability of hardware designs.
KW - FPV
KW - covert channel
KW - data leak
KW - flush.
KW - formal
KW - information flow
KW - microarchitectural
KW - temporal partitioning
KW - timing channel
KW - verification
UR - http://www.scopus.com/inward/record.url?scp=85174166221&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85174166221&partnerID=8YFLogxK
U2 - 10.1145/3613424.3614254
DO - 10.1145/3613424.3614254
M3 - Conference contribution
AN - SCOPUS:85174166221
T3 - Proceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2023
SP - 871
EP - 885
BT - Proceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2023
PB - Association for Computing Machinery, Inc
Y2 - 28 October 2023 through 1 November 2023
ER -