Bridging Theory and Practice:
Dependable Software and Secure systems

*This Lab. is not accepting new student.

OGAWA Laboratory
Professor：OGAWA Mizuhito

E-mail：
［Research areas］
Theoretical Computer Science, Formal Methods
［Keywords］
Formal language, Rewriting systems, Infinite state transition systems, Formal methods, SMT solver, Binary code analysis

Skills and background we are looking for in prospective students

Mathematical ability, e.g., deep understanding of discrete mathematics, mathematical logic, and combinatorics. The ability to reconstruct the definitions in your own words and show three non-trivial examples. English literacy, e.g., seminars of our lab are in English.

What you can expect to learn in this laboratory

Experience of the research methodology, i.e., clarify and define problems, consider approaches based on theory, concretize ideas, find/implement solutions, and report them. The research theme will be set depending on a student interest and ability. In the past, examples themes are mostly theory and tool implementation of formal methods, e.g., constraint solver (SMT solver raSAT), model checking for security protocol analysis, Java points-to analysis (Japot), binary code analysis (BE-PUM), roundoff error analysis, algebraic specification of SQL, and efficient implementation of model checking based on antichain algorithms. A student will experience a round of research through a case study on a specific topic. We think that a complete experience of such a round is more important than finishing the course in the standard periods.

【Job category of graduates】Academia (PhD), Software related industry (master)

Research outline

Our laboratory targets on the theoretical basis for the computational models, algorithms, and discrete mathematics, as well as their application for automated reasoning tools implementation. Typical theoretical topics are, graphs, ordering structures, rewriting systems, formal languages, mathematical logic and formal proofs. We are especially interested in finding relations among seemingly unrelated and finding new in the old. They are mostly by international collaborations.

1. Decidability in Well-Structured Pushdown Systems (WSPDS): By assuming the well-quasi-order (WQO) constraints on an infinite state transition system with a stack (named WSPDS), we can obtain many decidable properties for free, e.g., coverability and termination. WSPDS can uniformly formalize multi-thread programs and timed systems. (With Shanghai Jiaotong University, Nagoya University and Sankt Petersburg University) We further investigate on the relation between WQO and the regularity over various data structures. (With Ershov institute and Kazan Federal University)
2. Confluence of non-left-linear term rewriting system (TRS): Major properties of TRSs are confluence and termination. A well-known sufficient condition for the confluence of a TRS is left-linear and nonoverlapping, found in the 1970s. However, for a non-left-linear TRS, if right-linear and strongly nonoverlapping, it is conjectured confluent in 1990, which is left open. We are tackling this open problem. (With Nagoya University, Ecole Polytechnique and Tsinghua.)
3. SMT solver for nonlinear constraints over reals raSAT: Our original motivation was a reasoning engine for roundoff error analysis. We are developing an SMT solver raSAT, targeting on nonlinear constraints over reals. We have participated SMT-COMP QFNRA category from 2014, and we are ranked second from 2016,. following to Yices2 from CSL. (With University of Lorraine and VNU-Hanoi UET.)
4. Binary code analyzer BE-PUM for malware analysis: Although malware is usually small, its control structure is obfuscated and complex to bypass anti-virus software, e.g., self-modification (since the binary code has no distinctions between code and data), indirect jumps, and the sandbox detection using special Windows APIs. We are developing a binary code analyzer BE-PUM for x86/windows and ARM. An application is the packer identification. We are further extending the support for many platforms by using automatic formal semantics extraction from the instruction specification in English. (With VNU-HCMC HCMUT and University of Lorraine.)
5. Practically efficient algorithms for model checking: Finite automata and pushdown automata are often used for model checking, however, their complexity easily jumps to the exponential state explosion. A practically effective algorithm is using anti-chain, which are known for the determinization of finite automata. We have extended to Visibly Pushdown Automata (VPA) and currently try on alternating finite automata. (With Innsbruck University.)

Key publications

1. V.A.Vu, M.Ogawa: Formal Semantics Extraction from Natural Language Specifications for ARM. 23rd International Symposium on Formal Methods (FM 2019), LNCS 11800, 465-483, 2019.
2. M.Ogawa, V.L.Selivanov: On Classes of Regular Languages Related to Monotone WQOs. 21st International Conference on Descriptional Complexity of Formal Systems (DCFS 2019), LNCS 11612, 235-247, 2019.
3. T. X. Vu, V. K. To, M. Ogawa. raSAT : An SMT Solver for Polynomial Constraints. Formal Methods in System Design 51(3). 462-499, 2017.

Equipment

A standard note PC is enough.