Since the advent of Bitcoin in 2008, the interest in blockchain technology has surged tremendously. Numerous applications have been proposed in the field of finance, healthcare, and supply chain over the last decade. And, as the popularity of blockchains continue to rise, blockchain platforms must be enhanced to support new application needs. \nWe propose one such enhancement that is essential for financial applications and online marketplaces – support for time-based logic. Online marketplaces may need to validate transaction time-stamps against a perishable product’s expiry date to prevent sale of expired products. Similarly, financial applications in banking may also need a history of recent transactions for extending credit (like an overdraft) to a customer. As nodes in a blockchain operate in a distributed and trustless setting, it is imperative that they can access a global and trusted clock for verifying deadlines or examining a window of recent activity. \nIn this thesis, we present a lightweight solution that assigns time-stamps to blocks at transaction validation time, which can be referenced as a global clock by all nodes in the network. Moreover, our solution also maintains a cache \nreflecting the effects of recent transactions. We implement our solution, called TimeFabric, in Hyperledger Fabric, a popular permissioned blockchain platform, and experimentally demonstrate high throughput and minimal overhead (approximately 3%) of maintaining trusted time. We also demonstrate a 2x performance improvement due to the cache, compared to retrieving transaction histories directly from the ledger.
Benjamin Breiling, Bernhard Dieber, Martin Pinzger, Stefan Raß
With the growing popularity of robots, the development of robot applications is subject to an ever increasing number of additional requirements from e.g., safety, legal and ethical sides. The certification of an application for compliance to such requirements is an essential step in the development of a robot program. However, at this point in time it must be ensured that the integrity of this program is preserved meaning that no intentional or unintentional modifications happen to the program until the robot executes it. Based on the abstraction of robot programs as workflows we present in this work a cryptography-powered distributed infrastructure for the preservation of robot workflows. A client composes a robot program and once it is accepted a separate entity provides a digital signature for the workflow and its parameters which can be verified by the robot before executing it. We demonstrate a real-world implementation of this infrastructure using a mobile manipulator and its software stack. We also provide an outlook on the integration of this work into our larger undertaking to provide a distributed ledger-based compliant robot application development environment.
Nami Ashizawa, Naoto Yanai, Jason Paul Cruz, Shingo Okamura
Ethereum smart contracts are computer programs that are deployed and executed on the Ethereum blockchain to enforce agreements among untrusting parties. Being the most prominent platform that supports smart contracts, Ethereum has been targeted by many attacks and plagued by security incidents. Consequently, many smart contract vulnerabilities have been discovered in the past decade. To detect and prevent such vulnerabilities, different security analysis tools, including static and dynamic analysis tools, have been created, but their performance decreases drastically when codes to be analyzed are constantly being rewritten. In this paper, we propose Eth2Vec, a machine-learning-based static analysis tool that detects smart contract vulnerabilities. Eth2Vec maintains its robustness against code rewrites; i.e., it can detect vulnerabilities even in rewritten codes. Other machine-learning-based static analysis tools require features, which analysts create manually, as inputs. In contrast, Eth2Vec uses a neural network for language processing to automatically learn the features of vulnerable contracts. In doing so, Eth2Vec can detect vulnerabilities in smart contracts by comparing the similarities between the codes of a target contract and those of the learned contracts. We performed experiments with existing open databases, such as Etherscan, and Eth2Vec was able to outperform a recent model based on support vector machine in terms of well-known metrics, i.e., precision, recall, and F1-score.
Smart contracts are distributed, self-enforcing programs executing on top of blockchain networks. They have the potential to revolutionize many industries such as financial institutes and supply chains. However, smart contracts are subject to code-based vulnerabilities, which casts a shadow on its applications. As smart contracts are unpatchable (due to the immutability of blockchain), it is essential that smart contracts are guaranteed to be free of vulnerabilities. Unfortunately, smart contract languages such as Solidity are Turing-complete, which implies that verifying them statically is infeasible. Thus, alternative approaches must be developed to provide the guarantee. In this work, we develop an approach which automatically transforms smart contracts so that they are provably free of 4 common kinds of vulnerabilities. The key idea is to apply run-time verification in an efficient and provably correct manner. Experiment results with 5000 smart contracts show that our approach incurs minor run-time overhead in terms of time (i.e., 14.79%) and gas (i.e., 0.79%).
The relational database has become one of the mainstream tools for data storage and management. However, there are two main types of threats to relational databases: external attacks and internal tampering threats. In this paper, we focus on the internal tampering threats and propose a tamper-proof detection middleware named TDRB to provide efficient tamper-proof detection for relational databases. Within the TDRB middleware framework, raw data is still stored and queried from the relational database, while the hash digest of the critical data in the relational database is synchronously migrated to the blockchain for tamper detection. Based on this method, we leverage blockchain’s immutability to detect data tamper and maintain the advanced features of relational databases to better support ease of data persistence, complex queries, and large storage capacity. We also propose a performance improvement mechanism that involves connecting the blockchain and relational database to improve throughput and mitigate performance impact. A series of experiments indicate that the TDRB middleware can accurately detect the tampering information during arbitrary tampering with the relational database and the cache database. Compare with the baseline, with the increase of cache hit rate, the TDRB middleware query speed increased by 93.1%, update speed increased by 16.3%, delete speed increased by 16.1%, and join operation average speed increased by 95.2%. Given its generality, the TDRB middleware can be flexibly and conveniently integrated into third-party platforms.
Hyunyoung Oh, Kevin Nam, Seongil Jeon, Yeongpil Cho · 5 authors
Remote computing has emerged as a trendy computing model that enables users to process an immense number of computations efficiently on the remote server where the necessary data and high-performance computing power are provisioned. Unfortunately, despite such an advantage, this computing model suffers from insider threats that are committed by adversarial administrators of remote servers who attempt to steal or corrupt users' private data. These security threats are somewhat innate to remote computing in that there is no means to control administrators' unlimited data access. In this paper, we present our novel hardware-centric solution, called MeetGo, to address the intrinsic threats to remote computing. MeetGo is a field-programmable gate array (FPGA)-based trusted execution environment (TEE) that aims to operate independently of the host system architecture. To exhibit the ability and effectiveness of MeetGo as a TEE ensuring secure remote computing, we have built two concrete applications: cryptocurrency wallet and GPGPU. MeetGo provides a trust anchor for these applications that enable their users to trade cryptocurrency or to run a GPGPU program server on a remote server while staying safe from threats by insiders. Our experimental results clearly demonstrate that MeetGo incurs only a negligible performance overhead to the applications.
Open access
Security and Verification in Computing
Physical Unclonable Functions (PUFs) and Hardware Security
The success of Bitcoin since 2009 stimulates the development of other blockchain-based applications, such as Ethereum, a second generation of cryptocurrency which supports the revolutionary idea of smart contracts. An Ethereum smart contract is a computer program written in some domain-specific high-level programming languages, such as Solidity, Vyper, Bamboo, Flint, etc., and stored on the blockchain to achieve certain functionality. Smart contracts benefit from the features of the blockchain in various aspects. For instance, it is not necessary to have an external trusted authority to achieve consensus, and transactions through smart contracts are always traceable and credible. Smart contracts must be verified for multiple reasons. Firstly, due to the decentralized nature of the blockchain, smart contracts are different from programs written in other programming languages (e.g., C/Java). For instance, the storage of each contract instance is located at a permanent address on the blockchain. In this way, each contract instance is a particular execution context and context switches are possible through external calls. Particularly, in Solidity, delegatecall is executed in the context of the caller rather than the recipient, making it possible to modify the state of the caller. Programmers must be aware of the execution context of each statement to guarantee the programming correctness. Therefore, programming smart contracts is error-prone without a proper understanding of the underlying semantic model. Secondly, a smart contract can be deployed on the blockchain by any user in the network. Vulnerabilities in deployed contracts can be exploited to launch attacks that lead to huge financial loss. Verifying smart contracts against such vulnerabilities is crucial for protecting digital assets. One famous attack on smart contracts is the DAO attack in which the attacker exploited the reentrancy vulnerability and managed to take 60 million dollars under his/her control. Finally, it is very difficult, if not impossible, to patch a smart contract once it is deployed due to the very nature of the blockchain. There is a surge of interest in analyzing and verifying smart contracts. To the best of our knowledge, most of the existing approaches either focus on EVM (Ethereum Virtual Machine) bytecode, or translate Solidity smart contracts into programs in intermediate languages that are suitable for verifying smart contracts or detecting potential issues in associated verifiers or checkers. Furthermore, none of the existing works can directly handle smart contracts written in different high-level programming languages without translating them into EVM bytecode or intermediate languages. None of the existing approaches defines security properties with the high-level semantics of smart contracts. A direct executable formal semantics of the high-level smart contract programming language concerned is a must for both understanding and verifying smart contracts. Firstly, programmers write and reason about smart contracts at the level of source code without the semantics of which they are required to understand how Solidity programs are compiled into EVM bytecode in order to understand these contracts, which is far from trivial. In addition, there may be semantic gaps between high-level smart contract programming languages and low-level bytecode which are introduced by compiler bugs. In other words, after compilation the semantics of bytecode may not be equivalent to that of the corresponding high-level programs due to the compiler bugs involved. Therefore, both high-level and low-level semantics definitions are necessary to conduct equivalence checking to guarantee that security properties are preserved at both levels and reason about compiler bugs. Secondly, even though smart contracts can be transformed into programs in intermediate languages to be analyzed and verified in existing model checkers and verifiers, the equivalence checking of the high-level smart contract programming language concerned and the intermediate language applied to interpret it is crucial to the validity of the verification. We develop an executable operational semantics for the Solidity programming language to formally reason about smart contracts written in Solidity. The contributions of this work lie in four aspects. Firstly, our work is the first approach, to the best of our knowledge, to a complete executable formal semantics of Solidity constructed directly on the language itself other than Solidity compilers. The proposed executable semantics completely covers the supported high-level core features specified by the official Solidity documentation and is validated with the official compiler Remix. In addition, a new and general way of semantics formalization is applied in the semantics design, making the proposed semantics robust in the language evolution of smart contracts. Secondly, the proposed semantics provides a formal specification of smart contracts which solves the specification issues in the existing verification and analysis tools. Thirdly, the proposed semantics allows us to formally define semantic-level security properties for verifying smart contracts to exclude the false positives and negatives introduced by the existing approaches. Finally, the proposed semantics defines correct and secure high-level execution behaviours of smart contracts to reason about compiler bugs and assist developers in writing secure smart contracts. Furthermore, we develop a generalized formal semantic framework for smart contracts. The contributions of this work lie in three aspects. Firstly, our work is the first approach, to the best of our knowledge, to a generalized formal semantic framework for smart contracts which can directly handle contracts written in different high-level programming languages. Secondly, a general semantic model of smart contracts is constructed with rewriting logic in the K-framework. With the general semantic model, a direct executable formal semantics of a particular high-level smart contract programming language can be constructed as long as its core features fall into the ones defined in this model. The general semantic model is validated with its interpretation in Solidity using the Solidity compiler test set and evaluation results show that it is complete and correct. Lastly, the generated semantics facilitates the formal verification of smart contracts written in a particular high-level programming language as a formal specification of the corresponding language. Together with low-level specifications, it allows us to conduct equivalence checking on high-level contracts and low-level bytecode to reason about compiler bugs and guarantee that security properties are preserved at both levels. We define some security properties based on the formal semantics of the high-level smart contract programming languages. These security properties are defined from a general point of view and can be applied to detect a variety of vulnerabilities in smart contracts, such as the reentrancy vulnerability, exception disorders, integer underflows and overflows, etc. In addition, verification algorithms for these properties are constructed with the proposed semantic framework. We compare our approaches to the security analysis of smart contracts with the existing ones and highlight the importance of precise semantic foundations for the verification of smart contracts. Lastly, we systematize the existing approaches to the security analysis of smart contracts from the perspectives of domain-specific research and applications of general ideas to study the connection between the domain-specific issues in smart contracts and general analysis techniques. To conclude, this thesis studies the formal specification and verification of smart contracts, and combines domain-specific analysis and applications of general techniques. It also motivates other research directions related to the security analysis of smart contracts, such as the equivalence checking of high-level contracts and low-level bytecode, formal reasoning of high-level smart contract programming languages, the fairness analysis of smart contracts, etc.
Karim Baghery, Cyprien Delpech de Saint Guilhem, Emmanuela Orsini, Nigel P. Smart · 5 authors
This paper introduces M-Circuits, a program representation which generalizes arithmetic and binary circuits. This new representation is motivated by the way modern multi-party computation (MPC) systems based on linear secret sharing schemes actually operate. We then show how this representation also allows one to construct zero knowledge proof (ZKP) systems based on the MPC-in-the-head paradigm. The use of the M-Circuit program abstraction then allows for a number of program-specific optimizations to be applied generically. It also allows to separate complexity and security optimizations for program compilation from those for application protocols (MPC or ZKP).
Vladimir Kukharenko, Kirill Ziborov, Rafael Faritovich Sadykov, Ruslan Rezin
The extent of formal verification methods applied in industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain , is rapidly changing the situation. Since the main area of DLSs’ application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is largely determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is also required to ensure that the software implementation of the DLS nodes complies with this protocol. Finally, the verified software implementation of the protocol must run on a fairly reliable operating system. The financial focus of DLS application has also led to the emergence of the so-called smart contracts , which are an important part of the applied implementations of specific business processes based on DLSs. Therefore, the verifiability of smart contracts is also a critical requirement for industrial DLSs. In this paper, we describe an ongoing industrial project between a large Russian airline and three universities – Innopolis University (IU), Moscow Institute of Physics and Technology (MIPT) and Lomonosov Moscow State University (MSU). The main expected project result is a DLS for more flexible refueling of aircrafts, verified at least at the four technological levels described above. After brief project overview, we focus on our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes. The formal specification of the protocol is performed in the TLA+ language and then verified with a specialized TLC tool to verify models based on TLA+ specifications.
From weak clients outsourcing computational tasks to more powerful machines, to distributed blockchain nodes needing to agree on the state of the ledger in the presence of adversarial nodes, there is a growing need to efficiently verify the results of computations delegated to untrusted third parties. Verifiable computing is a new and interesting research area that addresses this problem. Recently, new applications of verifiable computing techniques have emerged in blockchain technology for secure key management, sybil-resistance and distributed consensus, and smart contracts, while providing desired performance and privacy guarantees. In this paper, we provide an overview of common methods for verifying computation and present how they are applied to blockchain technology. We group the presented verifiable computing applications into five main application areas, i.e., multiparty approval for secure key management, sybil-resistance and consensus, smart contracts and oracles, scalability, and privacy. The main contribution of this survey is to answer two research questions: 1) what are the main application areas of verifiable computing in blockchain technology, and 2) how are verifiable computing techniques used in major blockchain projects today.
Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács · 5 authors
Abstract Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a transfer operation. Currencies manipulated by code present a verification challenge to mathematically prove their integrity by reasoning about computer programs that operate over them, e.g., in Solidity. The ability to reason about sums is essential: even the simplest ERC-20 token standard of the Ethereum community provides a way to access the total supply of balances. Unfortunately, reasoning about code written against this interface is non-trivial: the number of addresses is unbounded, and establishing global invariants like the preservation of the sum of the balances by operations like transfer requires higher-order reasoning. In particular, automated reasoners do not provide ways to specify summations of arbitrary length. In this paper, we present a generalization of first-order logic which can express the unbounded sum of balances. We prove the decidablity of one of our extensions and the undecidability of a slightly richer one. We introduce first-order encodings to automate reasoning over software transitions with summations. We demonstrate the applicability of our results by using SMT solvers and first-order provers for validating the correctness of common transitions in smart contracts.
The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm.
Prior to provisioning sensor data to smart contracts, a pre-processing of the data on intermediate off-chain nodes is often necessary. When doing so, originally constructed cryptographic signatures cannot be verified on-chain anymore. This exposes an opportunity for undetected manipulation and presents a problem for applications in the Internet of Things where trustworthy sensor data is required on-chain. In this paper, we propose trustworthy pre-processing as enabler for end-to-end sensor data integrity in data on-chaining workflows. We define requirements for trustworthy pre-processing, present a model and common workflow for data on-chaining, select off-chain computation utilizing Zero-knowledge Proofs (ZKPs) and Trusted Execution Environments (TEEs) as promising solution approaches, and discuss both our proof-of-concept implementations and initial experimental, comparative evaluation results. The importance of trustworthy pre-processing and principle solution approaches are presented, addressing the major problem of end-to-end sensor data integrity in blockchain-based IoT applications.
Privacy-preservation and effective auditing are two desirable but challenging requirements on distributed ledgers. To meet the requirements, this paper presents an auditing scheme, called as AudiTEE, which can audit a distributed ledger in a generic, efficient, and privacy-preserving manner. AudiTEE leverages Trusted Execution Environment (TEE) to generate confidential but auditable transactions and realize arbitrary, efficient and confidential audit on them. Unfortunately, TEE suffers from some inherent barriers and is itself not a complete solution for fast audit. To tackle these challenges, AudiTEE takes advantage of KAMT (K-anonymity Authentication Based on Merkle Tree) protocol for efficient management on account and user-defined anonymous transactions. Further, to achieve a complete and fast audit with unlinkability, TEE doesn’t process through all but only a comparatively small part of transactions according to a special ktag attached on each transaction to ensure that a user cannot hide transactions from auditor even when auditor is blind with who is involved in each transaction on the ledger. Apart from the above, AudiTEE allows flexible control on user behaviors. We implement a concrete instance of AudiTEE under a bank setting and demonstrate the scalability with all its core functionalities.
Abstract A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This tool paper describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson’s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.
Yuichiro Chinen, Naoto Yanai, Jason Paul Cruz, Shingo Okamura
Ethereum smart contracts are programs that are deployed and executed in a consensus-based blockchain managed by a peer-to-peer network. Several re-entrancy attacks that aim to steal Ether, the cryptocurrency used in Ethereum, stored in deployed smart contracts have been found in the recent years. A countermeasure to such attacks is based on dynamic analysis that executes the smart contracts themselves, but it requires the spending of Ether and knowledge of attack patterns for analysis in advance. In this paper, we present a static analysis tool named RA (Re-entrancy Analyzer), a combination of symbolic execution and equivalence checking by a satisfiability modulo theories solver to analyze vulnerability of smart contracts to re-entrancy attacks. In contrast to existing tools, RA supports analysis of inter-contract behaviors by using only the Ethereum Virtual Machine bytecodes of target smart contracts, i.e., even without prior knowledge of attack patterns and without spending Ether. Furthermore, RA can verify existence of vulnerability to re-entrancy attacks without execution of smart contracts and it does not provide false positives and false negatives. We also present an implementation of RA to evaluate its performance in analyzing the vulnerability of deployed smart contracts to re-entrancy attacks and show that RA can precisely determine which smart contracts are vulnerable.
Decentralized finance (DeFi) has become one of the most successful applications of blockchain and smart contracts. The DeFi ecosystem enables a wide range of crypto-financial activities, while the underlying smart contracts often contain bugs, with many vulnerabilities arising from the unforeseen consequences of composing DeFi protocols together. In this paper, we propose a formal process-algebraic technique that models DeFi protocols in a compositional manner to allow for efficient property verification. We also conduct a case study to demonstrate the proposed approach in analyzing the composition of two interacting DeFi protocols, namely, Curve and Compound. Finally, we discuss how the proposed modeling and verification approach can be used to analyze financial and security properties of interest.
Jesús Correas, Pablo Gordillo, Guillermo Román‐Díez
Profiling tools have been widely used for studying the behavior of the programs with the objective of reducing the amount of resources consumed by them. Most profilers collect the information with dynamic techniques, i.e., execute an instrumented version of the program with some specific input arguments to profile the measures of interest. This article presents a novel static profiling technique for Ethereum smart contracts that, using static resource analysis, is able to generate upper-bound expressions that can be used to produce profiling information about the measure of interest. Unlike traditional profiling tools, we get upper-bounds on the measures of interest expressed in terms of the input arguments or the state variables of the smart contracts. The information that can be obtained by the upper-bounds allows us to detect gas-expensive fragments of a Solidity program or to spot resource-related vulnerabilities at specific program points of the program. Moreover, in this article we propose an automatic optimization of Solidity programs which reduces their gas consumption replacing the accesses to state variables by gas-efficient accesses to local variables. We have experimentally evaluated our technique and we have detected that 6.81% of the public functions analyzed can be optimized and 1.43% are vulnerable to execute arbitrary code.
Smart contract (SC) is an extension of BlockChain technology. Ethereum BlockChain was the first to incorporate SC and thus started a new era of crypto-currencies and electronic transactions. Solidity helps to program the SCs. Still, soon after Solidity's emergence in 2014, Solidity-based SCs suffered many attacks that deprived the SC account holders of their precious funds. The main reason for these attacks was the presence of vulnerabilities in SC. This paper discusses SC vulnerabilities and classifies them according to the domain knowledge of the faulty operations. This classification is a source of reminding developers and software engineers that for SC's safety, each SC requires proper testing with effective tools to catch those classes' vulnerabilities.
Leonid Al'bertovich Merkin-Janson, Ruslan Rezin, Nikolay Konstantinovich Vasilyev
In this paper we consider the software architecture of InnoChain, a distributed ledger system (DLS) with 5 levels of formal verification, including a formally-verified underlying operating system (OS). The objective of this architecture is to achieve a higher level of DLS dependability compared to more traditional software architectures and quality assurance (QA) methods. The architecture of InnoChain includes (1) a programming language for smart contracts which is a domain-specific language with formal semantics embedded into CakeML, which is a functional language ofthe ML family; this allows us to carry out formal verification of smart contracts' correctness properties using higher-order logic systems, such as HOL4; (2) trusted compilation of smart contracts into the machine code using the verified compiler available for CakeML, rather than relying on a virtual machine for execution of smart contracts; (3) using CakeML for implementation of InnoChain node functionality which allows for formal verification of code correctness and trusted compilation into the machine code; (4) formal verification of the consensus protocol used InnoChain, namely HotStuff BFT; (5) using seL4, a formally-verified microkernel, as the underlying OS for InnoChain instead of more traditional general-purpose OSes such as Linux. The proposed verified architecture will allow InnoChain to be used in mission-critical applications, such as the decentralized Aircraft Fuelling Control System which is currently under development for JSC Aeroflot, the Russian national air carrier.
Dec 16, 2020·CPP'2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 18--19, 2021, Virtual, Denmark
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language Elm. Our development is done in the context of the ConCert framework that enables smart contract verification. We contribute a verified boardroom voting smart contract featuring maximum voter privacy such that each vote is kept private except under collusion of all other parties. We also integrate property-based testing into ConCert using QuickChick and our development is the first to support testing properties of interacting smart contracts. We test several complex contracts such as a DAO-like contract, an escrow contract, an implementation of a Decentralized Finance (DeFi) contract which includes a custom token standard (Tezos FA2), and more. In total, this gives us a way to write dependent programs in Coq, test them semi-automatically, verify, and then extract to functional smart contract languages, while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.