Assistant Professor at Singapore Institute of Technology (SIT),
SIT Cibery-Security Research Group,
SIT System Section (S3),
Infocomm Technology,
Singapore Institute of Technology

My area of research goes from theoretical research related to formal methods to its application to different domains. In the more theoretical aspects, I work on concurrency, refinement, and inference systems, and programming language semantics, among others.

The non-theoretical side covers an heterogenous domain of applications in which I highlight micro-kernel security, quantum computing, smart-contracts, and hardware verification. I am also interested on the application of formal methods to 5G infrastructures, EV, IoT, Unmanned Vehicles and Mavlink protocol verification

I have recently being awarded with a Singapore MoE-Tier 1 project: MOSES: A Meta Executable Operational Semantics for Efficient Smart Contract Verification
In this project I aim to construct a meta-sematincs for smart-contract programming languages. This will be the base for an intermediate language to which translate smart-contracts developed in different languages, having a common verification framework based on that language

I am hiring a postdoc to work with me on this project, if you are interested please send me an email.

News

PC Member of PRDC 2023
PC Member of ICFEM 2023
PC Member of ICFEM 2022
Publication Accepted in POPL'22 . "Quantum Separation Logic: A Framework for Local Reasoning o Quantum Programs." PC Member of ICFEM 2021
Publication Accepted in ACM Transactions on Programming Languages and Systems (TOPLAS). "CSim2 : Compositional Top-down Verification of Concurrent Systems Using Rely-Guarantee". David Sanan, Yongwang Zhao, Shang-Wei Lin, Yang Liu "
Publication Accepted in IEEE Transactions on Vehicular Technology. "CANeleon: Protecting CAN Bus with Frame ID Chameleon". Kun Cheng, Yuebin Bai, Yuan Zhou, Yun Tang, David Sanan and Yang Liu "
PC Member of ICFEM 2020
Publication Accepted in S&P'20. "Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity. Jiao Jiao, Shuanglong Kan, Shang-Wei Lin, David Sanan, Yang Liu and Jun Sun "
Publication Accepted in CAV19. "Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS. Yongwang Zhao and David Sanan "
PC Member of ATVAART19
PC Member of ICFEM 2019 Doctoral Symposium
PC Member of Tacas18 Artifact Evaluation (TACASART'18)

Research

I am currently finishing a verification framework in Isabelle/HOL for quantum computing programs using separation logic. It is based on our work published in POPL'22, improving it and fixing a number of errors that I detected during the formalization. Once this is done, I plan to continue working on this line by adding incorrectness logic

I am also working on a very promising framework for the verification of sequential systems. The verification is highly automated among other things thanks to what we call phi-types. Phi-types introduce refinement in the verification assertions, allowing to reason over high level specifications, while the verification is done over low level specifications. This together with separation logic bring refinement to a new level enhancing its automation, becoming more powerful than just abstract refinement.

I keep working on compositional verification of concurrent systems, and its application to cyber-physical systems. I started this line when I was in NTU and thanks to it we were awarded with several NRF grants

Other research lines in which I worked in the past and that I still keep researching in is Micro-Kernel verification, from the source code to the machine code, using formal proofs. This involves the creation of frameworks and tools for the compositional verification of the micro-kernel from an abstract specification based on the ARINC-653 standard for partitioning micro-kernels. I verified some parts of a concurrent micro-kernel specification and its refinement with the implementation. The complexity of the verification of the micro-kernel makes necessary to have a team of several people working on the different verification tasks, in which I played a team coordinator role.

In relation to the micro-kernel verification, I worked also on the semantics of the SPARC v8+ ISA and weak memory models.

I have also collaborated on the formal verification of the Leon3 processor, a SPARC V8+ multi-core CPU and in the formalization of executable semantics for the RUST language for safe code generation, and in the research of compositional techniques for verification scalability.

Overall I am interested on anything related to formal methods and logic, and applying to real-world domains. I am open to collaborate on this topics

Recent Publications

  1. Ke Jiang, Tianwei Zhang, David Sanan,Yongwang Zhao, and Yang LiuA Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures. International Conference on Formal Engineering Methods (ICFEM'22)
  2. Xuan-Bach Le, Shang-Wei Lin, Sun Jun, David Sanan Quantum Separation Logic: A Framework for Local Reasoning o Quantum Programs. ACM SIGPLAN Symposium on Principle Of Programming Languages (POPL'22). January 2022. Pennsylvania
  3. David Sanan, Yongwang Zhao, Shang-Wei Lin, Yang Liu CSim2 : Compositional Top-down Verification of Concurrent Systems Using Rely-Guarantee. ACM Transactions on Programming Languages and Systems (TOPLAS)
  4. Xuan-Bach Le, David Sanan, Sun Jun, Shang-Wei Lin Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications. International Conference on Engineering of Complex Computer Systems (ICECCS)
  5. Zhé Hóu, David Sanan, Alwen Tiu, Yang Liu, Koh Chuen Hoa & Jin Song Dong An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model. Journal of Automated Reasoning
  6. Kun Cheng, Yuebin Bai, Yuan Zhou, Yun Tang, David Sanan and Yang Liu. CANeleon: Protecting CAN Bus with Frame ID Chameleon. IEEE Transactions on Vehicular Technology
  7. Jiao Jiao, Shuanglong Kan, Shang-Wei Lin, David Sanan, Yang Liu and Jun Sun. Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity. The 41st IEEE Symposium on Security and Privacy. May 2020. San Francisco US
  8. Wilayat Khan, David Sanan, Hou Zhe and Liu Yang. On Embedding a Hardware Description Language in Isabelle/HOL. Journal of Design Automation for Embedded Systems (DAEM).
  9. Ke Jiang, David Sanan, Yongwang Zhao, Shuanglong Kan and Yang Liu. OA Formally Verified Buddy Memory Allocation Model. The 24th International Conference on Engineering of Complex Computer Systems. November 2019. Guangzhou China.
  10. Yongwang Zhao, David Sanan, Fuyuan Zhang and Yang Liu. A Parametric Rely-guarantee Reasoning Framework for Concurrent Reactive Systems. The 3rd World Congress on Formal Methods (FM'19). October 2019, Porto Portugal
  11. Yongwang Zhao and David Sanan. Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS. The 31st International Conference on Computer-Aided Verification. July 2019, New York US
  12. Fuyuan Zhang, Yongwang Zhao, David Sanan, Yang Liu, Alwen Tiu, Shang-Wei Lin and Jun Sun. Compositional Reasoning for Shared-variable Concurrent Programs The 22nd International Symposium on Formal Methods. July 2018, Oxford UK
  13. Shang-Wei Lin, Jun Sun, Hao Xiao, Liu Yang, David Sanan, Henri Hansen. FiB: Squeezing Loop Invariants by Interpolation between Forward and Backward Reachability. The 32nd IEEE/ACM International Conference on Automated Software Engineering. October 30 – November 3, 2017. Urbana-Champaign, Illinois, USA
  14. Hou Zhe, David Sanan, Alwen Tiu, Yang Liu. Proof Tactics for Assertions in Separation Logic. 8th International Conference on Interactive Theorem Proving (ITP). 26-29 September 2017. Brasilia, Brazil.
  15. Yongwang Zhao, David Sanan, Fuyuan Zhang and Yang Liu. Refinement-based Specification and Security Analysis of Separation Kernels. IEEE Transactions on Dependable and Secure Computing. doi:10.1109/TDSC.2017.2672983
  16. David Sanan, Yongwang Zhao, Zhe Hou, Fuyuan Zhan, Alwen Tiu, Liu Yang. CSimpl: a Framework for the Verification of Concurrent Programs using Rely-Guarantee. 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 24-29 April 2017. Uppssala Sweden.
  17. Zhe Hou, David Sanan, Alwen Tiu, Liu Yang, Koh Chuen Hoa. An Executable Formalization of the SPARCv8 Instruction Set Architecture: A Case Study for the Leon3 Processor. 21st Internation Symposium on Formal Methods. LNICS 9995:388 – 405. November 9-11, 2016. Limassol Cyprus.
  18. Yongwang Zhao, David Sanan, Fuyuan Zhang, Yang Liu. Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 14-21 October 2016 Eindhoven, The Netherlands
  19. David Sanan, Yang Liu, Yongwang Zhao, Zhenchang Xing, Mike Hinchey. Verifying FreeRTOS' Cyclic Doubly LInked List Implementation: From Abstract Specification to Machine Code. 20th International Conference on Engineering of Complex Computer Systems. ICECCS 2015. 9-12 December 2015. Gold Coast, Australia.
  20. Yongwang Zhao, David Sanan, Fuyuan Zhang, Yang Liu. Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement. IEEE Transactions on Industrial Informatics 12(4):1321-1331

Research Experience

  1. PhD student at University of Málaga. From Dec 2004 to Nov 2009. Techniques for the Automatic Analysis of Software Described in Programming Languages
  2. Postdoc at University of Málaga. From Dec 2009 to May 2011. Extension of LTL with mu-calculus for the spatial and temporal verification of programs using complex data structures.
  3. Postdoc at Singapore University of Technology and Design. From Jun 2011 to Jun 2012. Application of model checking techniques to the verification of sensor networks software.
  4. Postdoc at Trinity College Dublin. From July 2012 to December 2013. Modelling and verification of a separation microkernel by means of theorem proving.
  5. Postdoc at National University of Singapore. From January 2014 to January 2015. Machine code verification by means of theorem proving.

Contact Me

SIT-Nanyang Polytechnic
172A Ang Mo Kio Avenue 8, Singapore 567739

Email: david.miguel AT singaporetech.edu.sg