UWSpace is currently experiencing technical difficulties resulting from its recent migration to a new version of its software. These technical issues are not affecting the submission and browse features of the site. UWaterloo community members may continue submitting items to UWSpace. We apologize for the inconvenience, and are actively working to resolve these technical issues.
 

Security Vulnerabilities in Smart Contracts as Specifications in Linear Temporal Logic

dc.contributor.authorRay, Indrani
dc.date.accessioned2021-12-21T13:52:15Z
dc.date.available2021-12-21T13:52:15Z
dc.date.issued2021-12-21
dc.date.submitted2020-12-10
dc.description.abstractEthereum is a distributed computer with a native cryptocurrency. Like other monetary transaction based systems, a problem this platform faces is accounts and transactions being susceptible to theft and other hacks. Smart contracts (programs which run on this blockchain) can store money and initiate financial transactions. They need to be carefully studied to safeguard against threats. This is especially true before deployment, as they become immutable after. Software analysis and verification techniques are applied to study security vulnerabilities in smart contracts. Currently, there are over 35 tools that do so. Many of them directly study contracts written in high level languages such as Solidity. In this work, we similarly study contracts, but at the lower bytecode level. We focus on different classes of smart contract vulnerabilities– access control, bad randomness, denial of service, front running, integer overflow/underflow, re-entrancy, short address, time manipulation, and unchecked low-level calls. We create specifications based on linear temporal logic to describe vulnerabilities in each of these categories, and we test them against real-world contracts.en
dc.identifier.urihttp://hdl.handle.net/10012/17791
dc.language.isoenen
dc.pendingfalse
dc.publisherUniversity of Waterlooen
dc.titleSecurity Vulnerabilities in Smart Contracts as Specifications in Linear Temporal Logicen
dc.typeMaster Thesisen
uws-etd.degreeMaster of Applied Scienceen
uws-etd.degree.departmentElectrical and Computer Engineeringen
uws-etd.degree.disciplineElectrical and Computer Engineeringen
uws-etd.degree.grantorUniversity of Waterlooen
uws-etd.embargo.terms0en
uws.contributor.advisorTripunitara, Mahesh
uws.contributor.affiliation1Faculty of Engineeringen
uws.peerReviewStatusUnrevieweden
uws.published.cityWaterlooen
uws.published.countryCanadaen
uws.published.provinceOntarioen
uws.scholarLevelGraduateen
uws.typeOfResourceTexten

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Ray_Indrani.pdf
Size:
2.06 MB
Format:
Adobe Portable Document Format
Description:
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
6.4 KB
Format:
Item-specific license agreed upon to submission
Description: