{"id":589363,"date":"2019-06-03T09:35:02","date_gmt":"2019-06-03T16:35:02","guid":{"rendered":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/?p=589363"},"modified":"2019-07-19T14:52:54","modified_gmt":"2019-07-19T21:52:54","slug":"researchers-work-to-secure-azure-blockchain-smart-contracts-with-formal-verification","status":"publish","type":"post","link":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/blog\/researchers-work-to-secure-azure-blockchain-smart-contracts-with-formal-verification\/","title":{"rendered":"Researchers work to secure Azure Blockchain smart contracts with formal verification"},"content":{"rendered":"

\"\"<\/a><\/p>\n

In its young existence, the tamperproof and distributed ledger technology blockchain has already generated a lot of buzz and is being seen as disruptive (opens in new tab)<\/span><\/a>, influencing approaches in such diverse areas as financial services, supply chains, and governance. To say its future is bright might be an understatement. According to Gartner, the technology is positioned to bring an added business value upward of $360 billion by 2026 (opens in new tab)<\/span><\/a>.<\/p>\n

One of the key drivers making blockchain-based applications programmable, accessible to enterprise customers, and able to meet the diverse needs of a variety of sectors is the smart contract, a type of software program running on top of the technology. Because of the immutable nature and extreme transparency inherent in smart contracts, they foster trust in adversarial environments, but also make it challenging to secure compared to traditional code.<\/p>\n

Recent high-profile breaches in public blockchains such as the The DAO exploit (opens in new tab)<\/span><\/a> and the Parity wallet bug (opens in new tab)<\/span><\/a>\u2014which resulted in the loss and freezing, respectively, of millions of dollars in cryptocurrency\u2014demonstrate what\u2019s at stake when vulnerabilities in smart contracts are exploited; they significantly undermine the trust in blockchain technologies. To make matters worse, performing bug fixes for smart contracts post-deployment is no small matter, incurring a great cost in both time and money.<\/p>\n

The Microsoft Azure Blockchain (opens in new tab)<\/span><\/a> team, which delivers products and services for creating, deploying, and managing end-to-end blockchain-powered applications (opens in new tab)<\/span><\/a> to enterprise customers, takes these threats seriously. Smart contracts play an integral role in their blockchain offerings\u2014from administering the governance of consortium members in Azure Blockchain Service (opens in new tab)<\/span><\/a> to implementing proof-of-concept solutions with Azure Blockchain Workbench (opens in new tab)<\/span><\/a>. The team also offers an Azure Blockchain development kit (opens in new tab)<\/span><\/a> for rapidly deploying smart contracts from Visual Studio Code (opens in new tab)<\/span><\/a>, Logic Apps (opens in new tab)<\/span><\/a>, and Microsoft Flow (opens in new tab)<\/span><\/a>.<\/p>\n

With a vision of fortifying smart contracts in Azure Blockchain, the team found a partner in researchers at Microsoft Research working on advanced techniques for ensuring correctness of software programs. The collaboration has resulted in VeriSol, a brand-new open-source formal verification tool (opens in new tab)<\/span><\/a> being developed by the researchers. With VeriSol\u2014short for Verifier for Solidity<\/a>\u2014developers can begin to express the desirable behaviors of smart contracts written in a subset of the popular Solidity language and then use mathematical logic machinery to rigorously check those specifications against the implementation. It has recently been incorporated into Azure Blockchain\u2019s continuous integration pipeline for smart contract development.<\/p>\n

\u201cVeriSol allows us to iterate more quickly because of the automatic and continuous checking, and it allows us to catch bugs faster without having to worry about potentially affecting customers,\u201d says Cody Born, Senior Software Engineer (opens in new tab)<\/span><\/a> on the Azure Blockchain team.<\/p>\n

Formal verification and smart contracts a perfect match<\/h3>\n

Formal verification has long been viewed as the only option to rigorous verification of safety-critical components in hardware (opens in new tab)<\/span><\/a> and software<\/a>. However, there is a caveat.<\/p>\n

\u201cThe use of formal verification for production software requires individuals skilled in highly specialized formal languages and tools, which imposes on development teams a steep learning cost and often several person-years of investment to break down the highly sophisticated task of verification into those that can be discharged mechanically by the verification tools,\u201d explains Microsoft Principal Researcher Shuvendu Lahiri<\/a>, one of several researchers behind VeriSol. \u201cSuch investment has confined the use and success of formal verification to a very small number of safety critical hardware and software components.\u201d<\/p>\n

But smart contracts possess several characteristics that make them a great candidate for bringing automated formal verification to mainstream smart contract developers.<\/p>\n

\u201cThe modest code size and the sequential execution semantics of smart contracts make them amenable to scalable verification, and the open operating environment substantially reduces the need to manually model the environment in which a smart contract operates,\u201d says Lahiri, who has spent the last decade leveraging and adapting formal verification<\/a> techniques for highly automated and high-coverage bug finding in operating system and browser components<\/a>.<\/p>\n

So Lahiri, Microsoft Senior Researcher and security expert Shuo Chen<\/a>, and The University of Texas at Austin\u2019s Yuepeng Wang (opens in new tab)<\/span><\/a>, a Microsoft intern at the time of the work, and Isil Dillig (opens in new tab)<\/span><\/a>, a visiting researcher, set out on a journey in the summer of 2018 to help Azure Blockchain\u2014and ultimately its customers\u2014author safer and higher-quality smart contracts.<\/p>\n

With VeriSol, Born and his fellow developers, including Microsoft Software Engineer Xinxing Liu (opens in new tab)<\/span><\/a>, can begin to specify and prove the security of their work in ways not feasible before. More traditional testing relies on developers\u2019 ability to foresee exactly how a product will be used, an exercise that involves some corner cases being overlooked, as humans can only think of so many different logical test cases, says Born. But formal verification automatically identifies the different ways the code could potentially violate a given invariant, including those cases developers can\u2019t predict.<\/p>\n

Smart contracts in Azure Blockchain<\/h3>\n

Even in its nascent existence, VeriSol has been applied to a diverse set of smart contracts in the Azure Blockchain ecosystem.<\/p>\n

In one application, the VeriSol team used the verifier to formalize and check specifications of the smart contracts that govern consortium members in Ethereum on Azure (opens in new tab)<\/span><\/a> and Azure Blockchain Service. The governance smart contracts are designed to efficiently manage memberships in a consortium setting, where\u2014unlike in public blockchains\u2014the ledger is restricted to a group of members who are aware of the identities of other members. Formal verification of such governance contracts can help ensure the management of membership\u2014how members are admitted and removed and how they vote on proposals and other matters, for example\u2014is carried out in the way Microsoft specified for its customers.<\/p>\n

In another study, the team applied VeriSol to smart contracts implementing proof-of-concept enterprise workflow applications on Azure Blockchain Workbench. A workflow application consists of a high-level workflow policy described as a state machine, where transitions are predicated by role-based access control (opens in new tab)<\/span><\/a>, and a Solidity smart contract that implements the state machine, along with the business logic, on the blockchain. It is crucial to the reliability and security of the application to ensure the Solidity program correctly implements the workflow policy, explains Lahiri. VeriSol was used to check the \u201csemantic conformance\u201d of such applications\u2014that is, that state machines implemented in the smart contract and specified in the workflow policy are never out of sync during deployment.<\/p>\n

\u201cMany enterprise multiparty workflows naturally fit into a state-machine pattern that can easily be represented by a smart contract,\u201d says Lahiri. \u201cThe ability to leverage the high-level workflow policies as formal specifications to be checked against Solidity code provides an exciting opportunity to bring formal verification seamlessly to customers of Workbench without the upfront burden of requiring explicit formal specifications from them.\u201d<\/p>\n

Along the way, VeriSol automatically revealed subtle bugs that were fixed during development and helped perform full correctness proofs of most properties and invariants with high levels of automation.<\/p>\n

Standing on the shoulder of giants<\/h3>\n

VeriSol operates by encoding the semantics of Solidity programs into the formal intermediate verification language Boogie (opens in new tab)<\/span><\/a> and leveraging and extending the Boogie verification toolchain. It supports high-coverage symbolic testing for finding counterexample traces automatically, as well as performing correctness proofs automatically or with some user guidance.<\/p>\n

VeriSol is built on a decade of work in verification already undertaken by Microsoft and its researchers as part of the company\u2019s larger commitment to security, the user experience, and high-quality, state-of-the-art products and services. That work includes such verification components as Z3 (opens in new tab)<\/span><\/a>, Corral<\/a>, and Boogie. These components, all of which are open-source, represent well-tested and established techniques without which VeriSol would not be possible.<\/p>\n

\"VeriSol\u2014short<\/a>

VeriSol\u2014short for Verifier for Solidity\u2014is a brand-new open-source formal verification tool being designed to improve the quality of smart contracts written in a subset of the Solidity language using the Boogie verification toolchain.<\/p><\/div>\n

However, the journey is far from complete.<\/p>\n

The VeriSol team is not only actively working toward supporting a large enough subset of Solidity that covers most enterprise smart contracts while keeping the verification tractable, but is also developing a code-contracts library to allow users to write expressive yet concise specifications and invariants without leaving the comforts of Solidity. Finally, they\u2019re investing in improving the automation in inferring common inductive invariants to reduce manual overhead for performing correctness proofs.<\/p>\n

While VeriSol is still a prototype primarily driven so far by smart contracts in Azure, the researchers have lofty goals for the verification tool and encourage open collaboration to help bring advances in formal verification to mainstream smart contract development.<\/p>\n

\u201cWe envision empowering not just Azure Blockchain developers and customers, but contributing to a full blockchain ecosystem that is safer and helping people realize the full potential of the technology without being plagued by the costly mistakes in smart contracts,\u201d says Lahiri.<\/p>\n","protected":false},"excerpt":{"rendered":"

In its young existence, the tamperproof and distributed ledger technology blockchain has already generated a lot of buzz and is being seen as disruptive, influencing approaches in such diverse areas as financial services, supply chains, and governance. To say its future is bright might be an understatement. According to Gartner, the technology is positioned to […]<\/p>\n","protected":false},"author":38022,"featured_media":590701,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":[],"msr_hide_image_in_river":0,"footnotes":""},"categories":[194488],"tags":[],"research-area":[13560],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-589363","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-program-languages-and-software-engineering","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[144812],"related-projects":[],"related-events":[],"related-researchers":[],"msr_type":"Post","featured_image_thumbnail":"\"\"","byline":"","formattedDate":"June 3, 2019","formattedExcerpt":"In its young existence, the tamperproof and distributed ledger technology blockchain has already generated a lot of buzz and is being seen as disruptive, influencing approaches in such diverse areas as financial services, supply chains, and governance. To say its future is bright might be…","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/posts\/589363","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/users\/38022"}],"replies":[{"embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/comments?post=589363"}],"version-history":[{"count":26,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/posts\/589363\/revisions"}],"predecessor-version":[{"id":598600,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/posts\/589363\/revisions\/598600"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/media\/590701"}],"wp:attachment":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/media?parent=589363"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/categories?post=589363"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/tags?post=589363"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=589363"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=589363"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=589363"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=589363"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=589363"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=589363"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=589363"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=589363"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}