{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/121552"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/121552","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Capturing the Ethereum virtual machine in the UC framework","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-12-04 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-12-04 without embargo terms","abstract_has_math":false,"creators":["Han, Fangqi"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Miller, Andrew"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2023,"date_issued":"2023-08","date_published":"2023-08","updated_at":"2026-07-22T22:25:00Z","subjects":["Security","Blockchain","Smart Contracts"],"languages":["en","eng"],"rights":["Copyright 2023 Fangqi Han"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/121552","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Miller, Andrew"]},{"key":"dc:creator","label":"Author","values":["Han, Fangqi"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2023-08","2023-07-19"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Security","Blockchain","Smart Contracts"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2023 Fangqi Han"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/121552"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-12-04 without embargo terms","The student, Fangqi Han, accepted the attached license on 2023-07-19 at 09:44.","The student, Fangqi Han, submitted this Thesis for approval on 2023-07-19 at 10:23.","This Thesis was approved for publication on 2023-07-19 at 11:33.","DSpace SAF Submission Ingestion Package generated from Vireo submission #19742 on 2023-12-04 at 17:03:26","Ethereum’s smart contract system has become a powerful platform for developing decentralized applications. Its introduction of programmability to blockchain systems has significantly expanded the use cases of blockchains. The technology that had been mostly used as a distributed ledger has now evolved into a distributed state machine, allowing developers to upload their programs to the blockchain and users to request execution of arbitrary computations by the platform. However, this exciting new advancement is not without risks. Attackers have been able to exploit various design flaws of Ethereum smart contracts and caused loss of highly valuable assets. On the other hand, security analyses of smart contract designs are often empirical and lack adoption of formal methods. Developers sometimes are only able to identify security breaches after attacks have been carried out. This is understandable, as the Ethereum smart contract system is difficult to capture, even by some of the most expressive frameworks that security analysts use to study distributed protocols. This work aims to provide a solution to this problem, by modeling the Ethereum Virtual Machine (EVM) as a global functionality in the Universal Composability (UC) framework and formulating proofs of smart contract security. It is our hope that formal proof techniques can receive wider adoption among developers of decentralized applications in the near future."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Capturing the Ethereum virtual machine in the UC framework"]}]}],"canonical_facts":{"dc:contributor":["Miller, Andrew"],"dc:creator":["Han, Fangqi"],"dc:date":["2023-08","2023-07-19"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-12-04 without embargo terms","The student, Fangqi Han, accepted the attached license on 2023-07-19 at 09:44.","The student, Fangqi Han, submitted this Thesis for approval on 2023-07-19 at 10:23.","This Thesis was approved for publication on 2023-07-19 at 11:33.","DSpace SAF Submission Ingestion Package generated from Vireo submission #19742 on 2023-12-04 at 17:03:26","Ethereum’s smart contract system has become a powerful platform for developing decentralized applications. Its introduction of programmability to blockchain systems has significantly expanded the use cases of blockchains. The technology that had been mostly used as a distributed ledger has now evolved into a distributed state machine, allowing developers to upload their programs to the blockchain and users to request execution of arbitrary computations by the platform. However, this exciting new advancement is not without risks. Attackers have been able to exploit various design flaws of Ethereum smart contracts and caused loss of highly valuable assets. On the other hand, security analyses of smart contract designs are often empirical and lack adoption of formal methods. Developers sometimes are only able to identify security breaches after attacks have been carried out. This is understandable, as the Ethereum smart contract system is difficult to capture, even by some of the most expressive frameworks that security analysts use to study distributed protocols. This work aims to provide a solution to this problem, by modeling the Ethereum Virtual Machine (EVM) as a global functionality in the Universal Composability (UC) framework and formulating proofs of smart contract security. It is our hope that formal proof techniques can receive wider adoption among developers of decentralized applications in the near future."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/121552"],"dc:language":["en","eng"],"dc:rights":["Copyright 2023 Fangqi Han"],"dc:subject":["Security","Blockchain","Smart Contracts"],"dc:title":["Capturing the Ethereum virtual machine in the UC framework"],"dc:type":["text"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:00Z"}