University of Toronto Computer Engineering Research Group (EECG)

Current Research Projects

The promise of decentralized ledger-based technologies (DLTs), or blockchain, has electrified the world and created an excitement for technology that was last seen in the 1990s when the internet was entering mainstream. The core premise of the technology is that DLT systems are secured by cryptography and economic incentives, and that they are governed by decentralized consensus. As such, it is critical that they are based on robust/sound economic and technology principles that enable fair governance and societal progress.

My current research topics are cross-disciplinary with the objective to define, research, and promote the technological, financial, privacy, security, and regulatory frameworks of DLT-based systems. I also work in the area of sentiment data analysis for fintech applications.


Smart Contract Automated Synthesis

 

The high cost and frequency of attacks against smart contract indicate that a move towards rigorous R&D practices in this field is inevitable. Automated software synthesis techniques which take as input a specification and possibly a high-level implementation and produce a low-level implementation of the target program are mandatory for correct-by-construction smart contracts that run on blockchains. To promote automated synthesis techniques and close the research gap, we work on the development of a template-based automated inductive synthesis framework for smart contracts, tightly integrated with the underlying smart contract language that is wrapped by a novel verification environment.  

 

Smart Contract Verification

 

As DLT systems grow and expand their reach across different applications, new security questions emerge that go to the heart of the technology. There are needs in improvements of software verification, formalism and standardization for the underlying smart contracts. In this project we develop a formal verification engine for smart contract programming languages such as Ethereum's Solidity and Libra's Move.

 

Crypto-Economic Analysis of Blockchain Systems

 

Economic incentives are the foundation for DLT systems as a result of their decentralized characteristic. As a centralized entity is absent in a DLT system, the duty of verifying key attributes of activities in the system relies on the system maintainers or the miners. Therefore, economically incentivized consensus mechanisms are critical to the security guarantee of a DLT system. We conduct economic analysis on existing DLT systems to improve their robustness against potential manipulations and aid design of new incentive mechanisms that safeguard their fairness and socioeconomic viability.

 

Decentralized Blockchain Oracles

 

As smart contracts cannot reach consensus on real world data outside the ledger itself, specialized smart contracts called oracles record such real world data in the ledger. Most oracles today do so without the robust security guarantees of the underlying ledger itself. Our group develops ASTRAEA, the first decentralized mechanism using game-theoretical incentives to record real-life events in a DLT, and continues to build improvements on it so to provide further robust security guarantees for data retrieval in permissionless or permissioned DLT systems.

 

Internet of Things (IoT)

 

The Internet of things is a system of interrelated (usually low-power) computing devices, mechanical and digital machines connected through a network to perform tasks without requiring control by a human. One of the limitations in the growth of IoT is this of their privacy and security, where DLT solutions present a transparent solution. The focus of this work is to develop and integrate DLT solutions to enhance the auditability, privacy, and security of modern IoT autonomous networks.

Former Research Projects

VLSI Design Debugging, Silicon Fault Diagnosis and Formal Methods

 

With the increase in the complexity of digital VLSI circuits, multiple design errors or/and manufacture defects can occur in a gate-level implementation or in a manufactured chip. In addition, due to recent advances in boolean satisfiability solvers, they have become a popular in VLSI CAD applications. The focus of this work is to develop efficient techniques for multiple fault/design error diagnosis using boolean satifiability solvers, as well as to optimize the satisfiability solver for this specific application. We also use our methodologies for fault diagnosis of different physical faults such as bridges, stuck-at faults and opens.

 

Design Verification

 

Functional verification is a hard problem with crucial time-to-market and financial consequences. It has been reported that the VLSI engineer dedicates at least 50% of his/her time to perform various verification related tasks. In this work we develop diagnosis-based verification techniques for designs with a degree of structural similarity. We use various formal equivalence engines (BDDs, ATPG, SAT-solvers etc) and we intend to apply our techniques to build efficient logic-to-logic verification tools.

 

Logic Optimization with Physical Level Considerations

 

Logic optimization is the step of the VLSI design cycle where a netlist is modified to reduce area, power consumption, switching noise or to improve the testability of the final circuit. We are interested in techniques that perform a sequence of simple logic transformations (design rewiring) until the desired constraints (usually defined at the logic and physical level) are satisfied. We also apply our techniques in a variety of different optimization and synthesis problems such as routing, synthesis for testability, low-power and delay.

 

Synthesis for Engineering Change

 

In a typical VLSI synthesis process specifications may change when the designer has already invested a significant amount of effort to get a design. Engineering changes to the original specification (RTL, HDL etc) may require large changes in the existing gate-level implementation if a conventional CAD tool is used. This is undesirable as it can jeopardize the engineering effort invested in the design. In this project we are interested for simulation/symbolic-based tools that can perform engineering changes efficiently.

  University of Toronto Computer Engineering Research Group (EECG)