[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

Alhabardi et al., 2022 - Google Patents

Verification of Bitcoin Script in Agda using weakest preconditions for access control

Alhabardi et al., 2022

View PDF
Document ID
3161014096343611195
Author
Alhabardi F
Beckmann A
Lazar B
Setzer A
Publication year
Publication venue
arXiv preprint arXiv:2203.03054

External Links

Snippet

This paper contributes to the verification of programs written in Bitcoin's smart contract language SCRIPT in the interactive theorem prover Agda. It focuses on the security property of access control for SCRIPT programs that govern the distribution of Bitcoins. It advocates …
Continue reading at arxiv.org (PDF) (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3604—Software analysis for verifying properties of programs
    • G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G06F8/43—Checking; Contextual analysis
    • G06F8/436—Semantic checking
    • G06F8/437—Type checking
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3668—Software testing
    • G06F11/3672—Test management
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/504—Formal methods
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/20—Handling natural language data
    • G06F17/27—Automatic analysis, e.g. parsing
    • G06F17/2705—Parsing
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/50—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
    • G06F21/57—Certifying or maintaining trusted computer platforms, e.g. secure boots or power-downs, version controls, system software checks, secure updates or assessing vulnerabilities
    • G06F21/577—Assessing vulnerabilities and evaluating computer system security
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/70—Software maintenance or management
    • G06F8/74—Reverse engineering; Extracting design information from source code
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/30—Creation or generation of source code
    • G06F8/35—Model driven
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/70—Software maintenance or management
    • G06F8/75—Structural analysis for program understanding
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/445—Programme loading or initiating
    • G06F9/44589—Programme code verification, e.g. Java bytecode verification, proof-carrying code
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/10—Requirements analysis; Specification techniques
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/20—Software design
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computer systems utilising knowledge based models
    • G06N5/02—Knowledge representation
    • G06N5/022—Knowledge engineering, knowledge acquisition

Similar Documents

Publication Publication Date Title
Almakhour et al. Verification of smart contracts: A survey
Annenkov et al. ConCert: a smart contract certification framework in Coq
Murray et al. Survey of formal verification methods for smart contracts on blockchain
Alhabardi et al. Verification of Bitcoin Script in Agda using weakest preconditions for access control
Yang et al. A hybrid formal verification system in coq for ensuring the reliability and security of ethereum-based service smart contracts
Malecha et al. Compositional computational reflection
Diatchki Improving Haskell types with SMT
Fedyukovich et al. Incremental verification of compiler optimizations
Küster Systematic validation of model transformations
Nelaturu et al. Correct-by-design interacting smart contracts and a systematic approach for verifying ERC20 and ERC721 contracts with VeriSolid
Singh et al. Formal verification and code generation for solidity smart contracts
Niemetz et al. Towards satisfiability modulo parametric bit-vectors
Coglio et al. Formal verification of zero-knowledge circuits
Gocht et al. End-to-end verification for subgraph solving
Antoy et al. Proving non-deterministic computations in Agda
Chlipala Formal reasoning about programs
Almakhour et al. On the verification of smart contracts: A systematic review
Vekris et al. Trust, but verify: Two-phase typing for dynamic languages
Hill et al. Proof-carrying plans: A resource logic for ai planning
Mustafa et al. Smart contract life-cycle management: an engineering framework for the generation of robust and verifiable smart contracts
Letychevskyi et al. Applying algebraic virtual machine to cybersecurity tasks
Cheng et al. Certifying a rule-based model transformation engine for proof preservation
Meng et al. Towards Developing Trusted Smart Contracts in Simulink.
Julliand et al. Generating tests from B specifications and dynamic selection criteria
Castanet et al. Generate certified test cases by combining theorem proving and reachability analysis