Kronos : verifying leak-free reset for a system-on-chip with multiple clock domains
Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, February, 2021
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2021
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/1721.1/130704 |
| _version_ | 1826206767278718976 |
|---|---|
| author | Moroze, Noah(Noah F.) |
| author2 | Anish Athalye, M. Frans Kaashoek and Nickolai Zeldovich. |
| author_facet | Anish Athalye, M. Frans Kaashoek and Nickolai Zeldovich. Moroze, Noah(Noah F.) |
| author_sort | Moroze, Noah(Noah F.) |
| collection | MIT |
| description | Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, February, 2021 |
| first_indexed | 2024-09-23T13:38:12Z |
| format | Thesis |
| id | mit-1721.1/130704 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T13:38:12Z |
| publishDate | 2021 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1307042021-05-25T03:20:41Z Kronos : verifying leak-free reset for a system-on-chip with multiple clock domains Verifying leak-free reset for a system-on-chip with multiple clock domains Moroze, Noah(Noah F.) Anish Athalye, M. Frans Kaashoek and Nickolai Zeldovich. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Electrical Engineering and Computer Science. Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, February, 2021 Cataloged from the official PDF of thesis. Includes bibliographical references (pages 97-99). Notary [3] uses formal verification to prove a hardware-level security property called deterministic start for a simple system-on-chip (SoC). Deterministic start requires that an SoC's state is fully reset by boot code to ensure that secrets cannot leak across reset boundaries. However, Notary's approach has several limitations. Its security property requires that all of the SoC's microarchitectural state can be reset to known values through software, and the property and proof technique apply only to SoCs with a single clock domain. These limitations prevent Notary's approach from being applied to more complex systems. This thesis addresses these limitations through Kronos, a system consisting of a verified SoC that satisfies a new security property called output determinism. Output determinism provides the same security guarantees as Notary without requiring that all of an SoC's state be reset by software. The SoC used in Kronos, called MicroTitan, is based on the open-source OpenTitan [16] and includes multiple clock domains. This thesis evaluates Kronos and demonstrates that existing open-source hardware can be modified to satisfy output determinism with minimal changes, and that the process of proving output determinism reveals hardware issues that violate desired security guarantees. by Noah Moroze. M. Eng. M.Eng. Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science 2021-05-24T19:52:27Z 2021-05-24T19:52:27Z 2021 2021 Thesis https://hdl.handle.net/1721.1/130704 1251800583 eng MIT theses may be protected by copyright. Please reuse MIT thesis content according to the MIT Libraries Permissions Policy, which is available through the URL provided. http://dspace.mit.edu/handle/1721.1/7582 99 pages application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Moroze, Noah(Noah F.) Kronos : verifying leak-free reset for a system-on-chip with multiple clock domains |
| title | Kronos : verifying leak-free reset for a system-on-chip with multiple clock domains |
| title_full | Kronos : verifying leak-free reset for a system-on-chip with multiple clock domains |
| title_fullStr | Kronos : verifying leak-free reset for a system-on-chip with multiple clock domains |
| title_full_unstemmed | Kronos : verifying leak-free reset for a system-on-chip with multiple clock domains |
| title_short | Kronos : verifying leak-free reset for a system-on-chip with multiple clock domains |
| title_sort | kronos verifying leak free reset for a system on chip with multiple clock domains |
| topic | Electrical Engineering and Computer Science. |
| url | https://hdl.handle.net/1721.1/130704 |
| work_keys_str_mv | AT morozenoahnoahf kronosverifyingleakfreeresetforasystemonchipwithmultipleclockdomains AT morozenoahnoahf verifyingleakfreeresetforasystemonchipwithmultipleclockdomains |