Research Projects

Blockchain technology has been successful in connecting companies, industries, and economies with transparency, security, and trust for over a decade. The support of smart contracts in blockchain is a major reason for its success. However, researchers face concerns about the safety and security of smart contracts, especially in critical systems. The literature lacks complete theoretical formalism, such as a complete abstract semantic model or detailed Verification Condition Generation approach. These approaches are specific to addressing safety and security concerns and cannot be extended to address additional issues like information flow vulnerabilities, runtime abort of smart contract execution due to overflow of gas cost consumption, or gas cost optimization. The existing proposals leave out an important construct 'loop', which needs special care in approximating the invariant property of the loop. This makes it difficult to extend these solutions for other blockchain platforms and languages. The objectives of this study are to sound approximation of run-time behavioral properties of smart contracts in various abstract domains, semantic-based information flow security analysis for confidentiality and integrity, code optimization for efficient smart contract code generation, deductive reasoning of smart contract codes using three approaches, smart contract code understanding and visualization, and the development of a language-independent formal methods-based toolchain based on these solutions.