Asavoae, Irina MariucaTofighi Shirazi, RamtineRiesco Rodríguez, AdriánYasuyoshi, Uemura2023-12-182023-12-182022Asăvoae, Irina Măriuca, et al. «Hardware Trojan Detection via Rewriting Logic». Journal of Logical and Algebraic Methods in Programming, vol. 127, junio de 2022, p. 100762. https://doi.org/10.1016/j.jlamp.2022.100762.2352-220810.1016/j.jlamp.2022.100762https://hdl.handle.net/20.500.14352/91467Hardware security studies, discovers, and classifies hardware attacks as well as defense strategies such as prevention and protection methods along the entire hardware production chain. Hardware Trojans represents a hardware attack model that emerged in the last decades in the hardware security community. In this paper, we present a methodology for achieving a scalable approach to detect hardware Trojans at the design stage using program transformation in a rewrite-based environment. We note that the hardware Trojan attack considered here assumes the vulnerability introduction during the hardware design stage while the payload is obtained as information leakage during the hardware usage. The main contribution in our work is the methodology correctness proof for a high security evaluation assurance level. We also benchmark the effectiveness of our methodology on industrial hardware designs, e.g., Advanced Encryption Standard cores, which is widely used and deployed for numerous devices and applications.engAttribution-NonCommercial-NoDerivatives 4.0 Internationalhttp://creativecommons.org/licenses/by-nc-nd/4.0/journal articlehttps://doi.org/10.1016/j.jlamp.2022.100762restricted accessInformática (Informática)1203.17 Informática