자료유형  

 학위논문

Control Number  

0016931332

International Standard Book Number  

9798379750794

Dewey Decimal Classification Number  

004

Main Entry-Personal Name  

Chen, Haoxian.

Publication, Distribution, etc. (Imprint  

[S.l.] : University of Pennsylvania., 2023

Publication, Distribution, etc. (Imprint  

Ann Arbor : ProQuest Dissertations & Theses, 2023

Physical Description  

1 online resource(145 p.)

General Note  

Source: Dissertations Abstracts International, Volume: 84-12, Section: A.

General Note  

Advisor: Loo, Boon Thau.

Dissertation Note  

Thesis (Ph.D.)--University of Pennsylvania, 2023.

Restrictions on Access Note  

This item must not be sold to any third party vendors.

Summary, Etc.  

요약Formal methods are essential in assuring system correctness. However, formal specification languages have steep learning curves, thus hindering broader application to system development in practice. To address this problem, we propose NetSpec, a tool that generates system specification via intuitive example-based interface, DeCon, a high-level language for Ethereum smart contracts that provides unified interfaces for contract implementation and specification, and DCV, a safety verification tool for DeCon.NetSpec aims to be i) highly expressive, capable of synthesizing network specifications with complex semantics; ii) scalable, by virtue of using a novel stochastic search algorithm to efficiently explore an unbounded solution space, and iii) robust, avoiding the need for exhaustive input-output examples by actively generating new examples. Our experiments demonstrate that NetSpec can synthesize a wide range of specifications used in network verification, analysis, and implementations. Furthermore, NetSpec improves upon existing approaches in terms of expressiveness, efficiency, and robustness to examples.DeCon, a specification language for Ethereum smart contracts, models a contract as a set of relational tables that store transaction records, driven by the observation that smart contract operations and contract-level properties can be naturally expressed as relational constraints. This relational representation enables convenient specification of contract properties, facilitates run-time monitoring of potential property violations, and brings clarity to debugging via data provenance. DeCon programs are compiled into executable Solidity programs, with instrumentation for run-time property monitoring. Our case studies demonstrate that DeCon can implement realistic smart contracts such as ERC20 and ERC721 digital tokens. The evaluation shows that DeCon has comparable efficiency with the open-source reference implementation, incurring 14% median gas overhead for execution, and another 16% median gas overhead for run-time verification.DCV is a sound and fully automatic verification tool for DeCon contracts. It proves safety properties by mathematical induction and can automatically infer inductive invariants without annotations from the developer. Our evaluation shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.

Subject Added Entry-Topical Term  

Computer science.

Subject Added Entry-Topical Term  

Computer engineering.

Subject Added Entry-Topical Term  

Information science.

Index Term-Uncontrolled  

Computer networks

Index Term-Uncontrolled  

Declarative programming

Index Term-Uncontrolled  

Program synthesis

Index Term-Uncontrolled  

Program verification

Index Term-Uncontrolled  

Smart contracts

Index Term-Uncontrolled  

NetSpec

Index Term-Uncontrolled  

DeCon

Added Entry-Corporate Name  

University of Pennsylvania Computer and Information Science

Host Item Entry  

Dissertations Abstracts International. 84-12A.

Host Item Entry  

Dissertation Abstract International

Electronic Location and Access  

로그인을 한후 보실 수 있는 자료입니다.

Control Number  

joongbu:641753