Mission-critical systems are those imperative systems whose failures can result in catastrophic consequences. Traditional techniques, such as manual investigation and testing, cannot ensure the absence of errors and security vulnerabilities within these systems. This dissertation leverages formal methods to comprehensively examine several mission-critical systems and their essential components. For each of these systems, we either provide a rigorous mathematical proof of its correctness, or use concrete reasoning to identify the underlying security issues. In the first part of this dissertation, we devise a method to prove that two systems are functionally equivalent modulo any timing differences. This method is based on symbolic model checking and induction, so it can generate a refinement mapping in addition to the verification result. In the second part, we propose an SAT-based attacking algorithm against sequential logic encryption, which does not require a working chip as the oracle. This study has established a new foundation for the security analysis of logic encryption. The third part investigates whether logic encryption can resist I/O attacks on deep neural networks. Our findings suggest that existing defence mechanisms are susceptible to quantitative analysis techniques.

Creator

• Li, You

DOI

• https://doi.org/10.21985/n2-q1bh-dx21

Subject

• Electrical engineering
• Computer engineering
• Computer science

Language

• en

Alternate Identifier

• http://dissertations.umi.com/northwestern:16748
• etdadmin_upload_1013532

Date created

• 2023-01-01

Resource type

• Dissertation

Rights statement

• In Copyright