Chan Ngo

Chan Ngo received his engineer's degree from Hanoi University of Technology with excellent ranking, his Master's degree in Computer Science (under a French government scholarship, Evariste Galois program) from Joseph Fourier University (University of Grenoble 1), and his Doctorate degree from Inria Rennes, France.

Chan is interested in design, implementation of systems-level programming languages, compilers, and formal verification for building reliable, certified software and hardware systems. A common theme is constructing correct embedded systems (i.e., control software in safety-critical systems, embedded system hardware designs) by applying formal verification including static analysis, model checking and correctness proof on the source code implementation, or mathematical models of these systems producing by model-based design toolchains, and formally certifying the correctness of the compilers and code generators in the model-based design toolchains.

Research Projects

• DANSE: The DANSE project focuses on the development of a new methodology to support evolving, adaptive and iterative System of Systems (SoS) life-cycle models based on a formal semantics for SoS inter-operations and supported by novel tools for analysis, simulation, and optimisation.
  DANSE includes industrial representatives with focus on aerospace, land, and automotive systems, as well as a leading tools and framework provider in the system space, and top European research institutes in system engineering. These partners have deep interest in the outcome of the research and are eager to deploy the developments as soon as they become available.
• DALI: The DALI project has undertaken a challenging agenda aimed at extending the people autonomous life beyond the home. The environment where the system operates is partially known (due to its large variability) and changing. Our assisted living device system must therefore acquire dynamic information about the user's immediate environment in order to guide its decision-making. The construction of a system of such complexity represents a major scientific and technological effort bringing together expertise across different disciplines.
• VERISYNC: The VERISYNC project aims at substantially improving the safety and reliability of embedded software that is being developed in the context of a Model-based design approach. This is achieved by formally proving the correctness of essential transformations that a model undergoes during its compilation to executable code. The definition of the semantics and the correctness proof of the compiler will be carried out by means of theorem proving. The compiler is executable and will be evaluated on realistic examples.
  The project is targeted at the compilation of a synchronous language to an imperative programming language. Synchronous languages have turned out to be an expressive formalism for embedded algorithms, and their precise semantics make them particularly suitable for our purpose.
• SCALP: Our day-to-day lives increasingly depend upon information and our ability to manipulate it securely. That is, in a way that prevents malicious elements to subvert the available information for their own benefits. This requires solutions based on cryptographic systems (primitives and protocols). However, no matter how carefully crafted cryptographic systems are, experience has shown that effective attacks can remain hidden for years. This may be caused by poor design or often unclear and poorly defined security properties and assumptions.
  Therefore, provable security, where new systems are published with a rigorous definition of their security goals and a mathematical proof that they meet their goals, is being increasingly advocated. While the adoption of provable security significantly increases, the complexity and diversity of designed systems tend to increase too. Hence, it is largely agreed on that the point has been reached where it is no longer viable to construct or verify cryptographic proofs by hand (Bellare and Rogaway 2004, Shoup 2004, Halevi 2005) and that there is a need for computer-aided verification methods for cryptographic systems. The goal of the SCALP project is to achieve a major step towards building automated tools for the verification of cryptographic systems. In order, to reconcile generality, imposed by the high diversity of cryptographic systems, and automation, we shall build our tools upon Coq.
• AVOTE: Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes. However, the convenience of electronic elections comes with a risk of large-scale fraud and their security has seriously been questioned. In the AVOTE project we propose to use formal methods to analyze electronic voting protocols.

Softwares

• PSCV: A runtime verification tool for probabilistic SystemC models. It consists of two components: the plugin for Plasma Lab in Java and tool for generating C++ monitor and aspect advices in C++, PSCV

• PLASMA Lab: PLASMA Lab is a compact, efficient and flexible platform for statistical model checking of stochastic models, PLASMA Lab
• Polychrony: The Polychrony toolset developed in C++ and Java, based on Signal, provides a formal framework to design, develop and validate critical systems, from abstract specification until deployment on distributed systems, Polychrony
• SigCert: The tool developed in OCaml checks the correctness of the compilation of Signal compiler w.r.t clock semantics, data dependence, and value-equivalence (not fully implemented), SigCert.tar.gz
• SigCV: PDS Simulation Relation Checking with SIGALI: implementation of the theory works in IFM 2012 article as the libraries in SIGALI toolset, SigCV.tar.gz
• Mobile Apps: Mobile applications: RATP, Turnstone, Saigon Places, A86, PhotoEnc,...on Apple App Store

Programming Blog

• Programming Embedded Software in Assembly, C/C++, and Ada for AVR, ARM, and Arduino Development Boards
• Mobile Embedded Applications on iOS and Android
• Software development in C/C++, C Sharp, Java, OCaml, and Python

Professional Activities

• 13th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'15), Austin, US, September 2015
• 8th International Conference on Language and Automata Theory and Applications (LATA'14), Madrid, Spain, March 2014