Secure Information Flow Verification with Mutable Dependent Types
| Autor: | G. Edward Suh, Andrew Ferraiuolo, Weizhe Hua, Andrew C. Myers |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
medicine.medical_specialty
business.industry Computer science Hardware description language Computer security compromised by hardware failure 02 engineering and technology 020202 computer hardware & architecture Hardware register 020204 information systems Embedded system 0202 electrical engineering electronic engineering information engineering medicine Hardware compatibility list Hardware design languages Information flow (information theory) business Hardware_REGISTER-TRANSFER-LEVELIMPLEMENTATION computer computer.programming_language |
| Zdroj: | DAC |
| DOI: | 10.1145/3061639.3062316 |
| Popis: | This paper presents a novel secure hardware description language (HDL) that uses an information flow type system to ensure that hardware is secure at design time. The novelty of this HDL lies in its ability to securely share hardware modules and storage elements across multiple security levels. Unlike previous secure HDLs, the new HDL enables secure sharing at a fine granularity and without implicitly adding hardware for security enforcement; this is important because the implicitly added hardware can break functionality and harm efficiency. The new HDL enables practical hardware designs that are secure, correct, and efficient. We demonstrate the practicality of the new HDL by using it to design and type-check a synthesizable pipelined processor implementation that support protection rings and instructions that change modes. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|