國立虎尾科技大學 |

Formal Verification Techniques for Microprocessor Security /

Record Type:	Language materials, printed : Monograph/item
Title/Author:	Formal Verification Techniques for Microprocessor Security // Nimish Mathure.
Author:	Mathure, Nimish,
Description:	1 electronic resource (120 pages)
Notes:	Source: Dissertations Abstracts International, Volume: 86-03, Section: B.
Contained By:	Dissertations Abstracts International86-03B.
Subject:	Computer engineering. -
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=31329397
ISBN:	9798384103424

Formal Verification Techniques for Microprocessor Security /
Mathure, Nimish,

Formal Verification Techniques for Microprocessor Security /Nimish Mathure. - 1 electronic resource (120 pages)

Source: Dissertations Abstracts International, Volume: 86-03, Section: B.

Microprocessor security is a pressing concern in our rapidly evolving digital systems, where vulnerabilities can lead to a catastrophic consequences. Recent transient execution attack such as Spectre and Micro-architectural data sampling attack such as Rouge In-flight Data Load have demonstrated the urgent need for robust defenses. These attacks exploits the vulnerabilities of the microprocessor caused due to speculative execution, posing significant risks to sensitive data. Consequently several security mitigation methods are proposed in addressing the novel threats. However, the security measures can fall short on addressing the threats, can be infected with hardware Trojans or can be susceptible to bugs in implementation. Formal verification emerges as a potent tool in this context. Formal verification employs mathematical models and propositional logic to rigorously assess microprocessor design's correctness and security properties. In context of security attacks, formal verification can be employed to assess the robustness of the security measures as well as identify any vulnerabilities before they can be exploited. This dissertation encompasses security mitigation methodologies against such attacks as well as the vital connection between microprocessor security and formal verification. Firstly addressed is the intricate challenge of designing and detecting hardware Trojans within a in-ordered pipelined microprocessor circuit. Secondly, the dissertation explores the security attacks with specific focus on Spectre and Rogue In-flight Data Load, the security measures against them, as well as formal verification methodologies tailored for identifying microprocessor architecture design's vulnerability towards the attacks. Also detecting vulnerabilities in microprocessors which employ security measures, caused due to inadequacies in implementation, trojans or bugs. The methodologies proposed within this work demonstrated a detection rate of 100% over several benchmarks, highlighting the effectiveness and reliability.

English

ISBN: 9798384103424Subjects--Topical Terms:

569006
Computer engineering.
Subjects--Index Terms:

Formal verification

Formal Verification Techniques for Microprocessor Security /
LDR:03541nam a22004333i 4500 001 1157815
005 20250603111420.5
006 m o d
007 cr|nu||||||||
008 250804s2024 miu||||||m |||||||eng d
020 $a 9798384103424
035 $a (MiAaPQD)AAI31329397
035 $a AAI31329397
040 $a MiAaPQD $b eng $c MiAaPQD $e rda
100 1 $a Mathure, Nimish, $e author. $0 (orcid)0000-0002-0508-3621 $3 1484091
245 1 0 $a Formal Verification Techniques for Microprocessor Security / $c Nimish Mathure.
264 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2024
300 $a 1 electronic resource (120 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertations Abstracts International, Volume: 86-03, Section: B.
500 $a Advisors: Srinivasan, Sudarshan K. Committee members: Huang, Ying; Wang, Danling; George, Sumitha.
502 $b Ph.D. $c North Dakota State University $d 2024.
520 $a Microprocessor security is a pressing concern in our rapidly evolving digital systems, where vulnerabilities can lead to a catastrophic consequences. Recent transient execution attack such as Spectre and Micro-architectural data sampling attack such as Rouge In-flight Data Load have demonstrated the urgent need for robust defenses. These attacks exploits the vulnerabilities of the microprocessor caused due to speculative execution, posing significant risks to sensitive data. Consequently several security mitigation methods are proposed in addressing the novel threats. However, the security measures can fall short on addressing the threats, can be infected with hardware Trojans or can be susceptible to bugs in implementation. Formal verification emerges as a potent tool in this context. Formal verification employs mathematical models and propositional logic to rigorously assess microprocessor design's correctness and security properties. In context of security attacks, formal verification can be employed to assess the robustness of the security measures as well as identify any vulnerabilities before they can be exploited. This dissertation encompasses security mitigation methodologies against such attacks as well as the vital connection between microprocessor security and formal verification. Firstly addressed is the intricate challenge of designing and detecting hardware Trojans within a in-ordered pipelined microprocessor circuit. Secondly, the dissertation explores the security attacks with specific focus on Spectre and Rogue In-flight Data Load, the security measures against them, as well as formal verification methodologies tailored for identifying microprocessor architecture design's vulnerability towards the attacks. Also detecting vulnerabilities in microprocessors which employ security measures, caused due to inadequacies in implementation, trojans or bugs. The methodologies proposed within this work demonstrated a detection rate of 100% over several benchmarks, highlighting the effectiveness and reliability.
546 $a English
590 $a School code: 0157
650 4 $a Computer engineering. $3 569006
650 4 $a Engineering. $3 561152
650 4 $a Computer science. $3 573171
650 4 $a Electrical engineering. $3 596380
653 $a Formal verification
653 $a Hardware Trojans
653 $a Microprocessor security
653 $a Transient execution attack
690 $a 0464
690 $a 0544
690 $a 0984
690 $a 0537
710 2 $a North Dakota State University. $b Electrical and Computer Engineering. $3 1182288
720 1 $a Srinivasan, Sudarshan K. $e degree supervisor.
773 0 $t Dissertations Abstracts International $g 86-03B.
790 $a 0157
791 $a Ph.D.
792 $a 2024
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=31329397