Towards Verifiably Secure Systems-on-Chip Platforms
Autor: | Pramod Subramanyan, Sujit Kumar Muduli |
---|---|
Rok vydání: | 2019 |
Předmět: |
Functional verification
Computer science Firmware business.industry Formal semantics (linguistics) 02 engineering and technology Adversary computer.software_genre 020202 computer hardware & architecture 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Property Specification Language Software engineering business computer Formal verification Protocol (object-oriented programming) Verification and validation computer.programming_language |
Zdroj: | ATS |
DOI: | 10.1109/ats47505.2019.00017 |
Popis: | Verification and validation of system-level security primitives is a pressing challenge in systems-on-chip (SoC) design and verification. This is a difficult problem to tackle for three reasons. First, no general frameworks exist that can enable adversary modeling for SoC platforms. Second, succinct specification of the desired security properties is not possible with current property specification languages. Finally, verification of a security specification is more challenging than functional verification. In this paper, we introduce a formal framework that enables general adversary modeling for SoC platforms and a security property specification language for this framework. We present formal semantics for the framework and illustrate its utility through a case study of an authenticated firmware load protocol. |
Databáze: | OpenAIRE |
Externí odkaz: |