{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/122053"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/122053","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Mechanized proofs that hardware is safe from timing attacks","abstract":"A recurring problem in cryptography engineering is the potential for secret data to be leaked through aspects of software and hardware that are orthogonal to functional correctness. In particular, much effort is put into writing cryptography code whose timing behavior - how many CPU clock cycles it takes to complete a given cryptographic operation - is independent of any secret inputs to that operation. This is a difficult problem because it depends not only on the code itself, but also on various optimizations such as branch prediction and memory caching implemented by the underlying hardware the program runs on. We make use of Kami, a domain-specific language for describing and formally verifying hardware modules, to build a system for constructing machine-checked proofs that a given piece of code running on a given RISC-V CPU design will not leak secret inputs through timing behavior. Our system allows software and hardware to be analyzed and verified independently, and we prove that any combination of software and hardware that meet our validation criteria will be safe from timing-based side channels. We demonstrate an example of validating a real cryptographic program and a concrete RISC-V CPU using our system, illustrating the applicability of our tools and laying the groundwork for validating more complex programs and CPUs.","abstract_html":"A recurring problem in cryptography engineering is the potential for secret data to be leaked through aspects of software and hardware that are orthogonal to functional correctness. In particular, much effort is put into writing cryptography code whose timing behavior - how many CPU clock cycles it takes to complete a given cryptographic operation - is independent of any secret inputs to that operation. This is a difficult problem because it depends not only on the code itself, but also on various optimizations such as branch prediction and memory caching implemented by the underlying hardware the program runs on. We make use of Kami, a domain-specific language for describing and formally verifying hardware modules, to build a system for constructing machine-checked proofs that a given piece of code running on a given RISC-V CPU design will not leak secret inputs through timing behavior. Our system allows software and hardware to be analyzed and verified independently, and we prove that any combination of software and hardware that meet our validation criteria will be safe from timing-based side channels. We demonstrate an example of validating a real cryptographic program and a concrete RISC-V CPU using our system, illustrating the applicability of our tools and laying the groundwork for validating more complex programs and CPUs.","abstract_has_math":false,"creators":["Duxovni, Faye(Faye Samara)"],"institution":"Massachusetts Institute of Technology","degree_name":"Master","degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","school":null,"contributors":[],"advisors":["Adam Chlipala."],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018","date_published":"2018","updated_at":"2026-07-22T22:21:49Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"rights":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/122053","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Adam Chlipala."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","EECS"]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Duxovni, Faye(Faye Samara)"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2019-09-11T21:55:20Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2019-09-11T21:55:20Z"]},{"key":"dc:date.issued","label":"Date","values":["2018"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/122053"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2018","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 47-48)."]},{"key":"dc:description.abstract","label":"Abstract","values":["A recurring problem in cryptography engineering is the potential for secret data to be leaked through aspects of software and hardware that are orthogonal to functional correctness. In particular, much effort is put into writing cryptography code whose timing behavior - how many CPU clock cycles it takes to complete a given cryptographic operation - is independent of any secret inputs to that operation. This is a difficult problem because it depends not only on the code itself, but also on various optimizations such as branch prediction and memory caching implemented by the underlying hardware the program runs on. We make use of Kami, a domain-specific language for describing and formally verifying hardware modules, to build a system for constructing machine-checked proofs that a given piece of code running on a given RISC-V CPU design will not leak secret inputs through timing behavior. Our system allows software and hardware to be analyzed and verified independently, and we prove that any combination of software and hardware that meet our validation criteria will be safe from timing-based side channels. We demonstrate an example of validating a real cryptographic program and a concrete RISC-V CPU using our system, illustrating the applicability of our tools and laying the groundwork for validating more complex programs and CPUs."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M. Eng."]},{"key":"dc:title","label":"Title","values":["Mechanized proofs that hardware is safe from timing attacks"]}]}],"canonical_facts":{"dc:contributor.advisor":["Adam Chlipala."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","EECS"],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Duxovni, Faye(Faye Samara)"],"dc:date.accessioned":["2019-09-11T21:55:20Z"],"dc:date.available":["2019-09-11T21:55:20Z"],"dc:date.issued":["2018"],"dc:description":["This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2018","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 47-48)."],"dc:description.abstract":["A recurring problem in cryptography engineering is the potential for secret data to be leaked through aspects of software and hardware that are orthogonal to functional correctness. In particular, much effort is put into writing cryptography code whose timing behavior - how many CPU clock cycles it takes to complete a given cryptographic operation - is independent of any secret inputs to that operation. This is a difficult problem because it depends not only on the code itself, but also on various optimizations such as branch prediction and memory caching implemented by the underlying hardware the program runs on. We make use of Kami, a domain-specific language for describing and formally verifying hardware modules, to build a system for constructing machine-checked proofs that a given piece of code running on a given RISC-V CPU design will not leak secret inputs through timing behavior. Our system allows software and hardware to be analyzed and verified independently, and we prove that any combination of software and hardware that meet our validation criteria will be safe from timing-based side channels. We demonstrate an example of validating a real cryptographic program and a concrete RISC-V CPU using our system, illustrating the applicability of our tools and laying the groundwork for validating more complex programs and CPUs."],"dc:description.degree":["M. Eng."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/122053"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Mechanized proofs that hardware is safe from timing attacks"],"dc:type":["Thesis"],"thesis:degree_name":["Master"]},"updated_at":"2026-07-22T22:21:49Z"}