{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/100294"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/100294","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Memory-safe microcontroller applications with the Bedrock structured programming system","abstract":"Microcontrollers - low-power, real-mode CPUS - drive digital electronics all over the world, making their safety and reliability critical. However, microcontrollers generally lack the memory protection common in desktop processors, so memory safety must come through other means. One such mechanism is Bedrock, a library for the Coq proof assistant that applies separation logic to a small c-like language, allowing programmers to prove memory-related properties about their code. I used Bedrock to build a security peripheral out of a Cortex-m3 microcontroller; my peripheral provides both AES encryption and append-only logging to a host system, and I showed the software it runs is memory-safe. Working with Bedrock was challenging but rewarding, and it provides a glimpse into a future where system programmers can prove code correct as a matter of course.","abstract_html":"Microcontrollers - low-power, real-mode CPUS - drive digital electronics all over the world, making their safety and reliability critical. However, microcontrollers generally lack the memory protection common in desktop processors, so memory safety must come through other means. One such mechanism is Bedrock, a library for the Coq proof assistant that applies separation logic to a small c-like language, allowing programmers to prove memory-related properties about their code. I used Bedrock to build a security peripheral out of a Cortex-m3 microcontroller; my peripheral provides both AES encryption and append-only logging to a host system, and I showed the software it runs is memory-safe. Working with Bedrock was challenging but rewarding, and it provides a glimpse into a future where system programmers can prove code correct as a matter of course.","abstract_has_math":false,"creators":["Barenblat, Benjamin Ezra"],"institution":"Massachusetts Institute of Technology","degree_name":null,"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":2015,"date_issued":"2015","date_published":"2015","updated_at":"2026-07-22T22:22:22Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/100294","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."]},{"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":["Barenblat, Benjamin Ezra"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2015-12-16T15:54:00Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2015-12-16T15:54:00Z"]},{"key":"dc:date.issued","label":"Date","values":["2015"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"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":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about 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":["http://hdl.handle.net/1721.1/100294"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2015.","This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 71-72)."]},{"key":"dc:description.abstract","label":"Abstract","values":["Microcontrollers - low-power, real-mode CPUS - drive digital electronics all over the world, making their safety and reliability critical. However, microcontrollers generally lack the memory protection common in desktop processors, so memory safety must come through other means. One such mechanism is Bedrock, a library for the Coq proof assistant that applies separation logic to a small c-like language, allowing programmers to prove memory-related properties about their code. I used Bedrock to build a security peripheral out of a Cortex-m3 microcontroller; my peripheral provides both AES encryption and append-only logging to a host system, and I showed the software it runs is memory-safe. Working with Bedrock was challenging but rewarding, and it provides a glimpse into a future where system programmers can prove code correct as a matter of course."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M. Eng."]},{"key":"dc:title","label":"Title","values":["Memory-safe microcontroller applications with the Bedrock structured programming system"]}]}],"canonical_facts":{"dc:contributor.advisor":["Adam Chlipala."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Barenblat, Benjamin Ezra"],"dc:date.accessioned":["2015-12-16T15:54:00Z"],"dc:date.available":["2015-12-16T15:54:00Z"],"dc:date.issued":["2015"],"dc:description":["Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2015.","This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 71-72)."],"dc:description.abstract":["Microcontrollers - low-power, real-mode CPUS - drive digital electronics all over the world, making their safety and reliability critical. However, microcontrollers generally lack the memory protection common in desktop processors, so memory safety must come through other means. One such mechanism is Bedrock, a library for the Coq proof assistant that applies separation logic to a small c-like language, allowing programmers to prove memory-related properties about their code. I used Bedrock to build a security peripheral out of a Cortex-m3 microcontroller; my peripheral provides both AES encryption and append-only logging to a host system, and I showed the software it runs is memory-safe. Working with Bedrock was challenging but rewarding, and it provides a glimpse into a future where system programmers can prove code correct as a matter of course."],"dc:description.degree":["M. Eng."],"dc:identifier.uri":["http://hdl.handle.net/1721.1/100294"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Memory-safe microcontroller applications with the Bedrock structured programming system"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:22:22Z"}