These are technical systems that operate within a legal or regulatory context, and the verification of correctness and security properties (for example, of smart contracts), requires reasoning about both programs and laws. For example, compliance with a smart tenancy agreement requires reasoning about the code in the smart contract along with the relevant law on rental agreements.
Professor Stephen Chong — "We are working on designing and implementing a model checker for Ethereum bytecode. Model checkers can exhaustively test properties of software and either verify that the property holds or produce a counter-example to demonstrate why it does not hold. We are exploring security properties that apply to most Ethereum smart contracts and can be checked by our model checker, as well as allowing smart-contract developers to check properties that are specific to their contract. Our work allows security checking to focus on the actual desired security outcome, instead of focusing on the particular mechanism by which a smart contract is attacked. More broadly, we are investigating the use of formal methods to reason about cyber-legal systems: computer systems that operate within legal or regulatory restrictions.
We are also developing an authorization logic to reason about trust in computation. Authorization logics provide a formal approach to reason about who is permitted (authorized) to perform actions, and the trust relationships between entities. The novel authorization logic that we are developing extends traditional authorization logic with expressive mechanisms to specify trust in computation. For example, with respect to blockchain smart contracts, the logic would allow an account to specify that it trusts a specific contract already on the blockchain or—more interestingly—that it trusts any account that has been analyzed by our model checker and proven to satisfy some standard security properties."