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.

Central Bank Digital Currencies

Today's societal digitization continues to advance at exponential speeds driven by technology trends. Billions of Internet of Things devices have made their way into our daily lives, but also into healthcare, manufacturing, and supplychains. In contrast, the financial sector still largely operates on legacy infrastructures, where merchants receive their payments long after they released the digital/physical good to the consumer. In addition, the emergence of Decentralized Finance through blockchain technology, and the accumulation of data in private silos, have demonstrated a capacity to impact national sovereignty and monetary transmission channels. Against this backdrop, many central banks have recently started to research and test the issuance of digitally native fiat money or Central Bank Digital Currencies (CBDCs)in an effort to redesign the essence and use of physical cash. CBDCs present a broad variety of designs, which translate into manifold techno-legal and standardization policy questions. In this context, our research addresses the state-of-the-art of CBDCs with a specific focus on retail CBDCs, with a focus on of candidate architectures, techno-legal questions (more notably privacy and AML/CFT) and regulatory compliance.

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.  

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.

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.

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.

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 with a focus on V2X (vehicle-to-vehicle) applications.

Machine Learning for Fintech Applications

In this topic we work along side with colleagues from Rotman School of Management to develop machine learning applications for sentiment analysis of financial instruments.

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.

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 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.

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.