David Miguel Sanan Baena

David Miguel Sanan Baena

Assistant Professor

Singapore Institute of Technology

Biography

Dr. David Sanan received his PhD degree in Software Engineering from the University of Malaga, Malaga, Spain, in 2009. Before joining SIT as an Assistant Professor, he was a Principal Research Scientist at Nanyang Technological University where he was leading several projects at the CyberSecurity Lab. Previously, he was a researcher at some prestigious universities like Trinity College Dublin and National University of Singapore.

His research interest is in bringing together theoretical research and applications, by applying formal methods to guarantee the security of real-world applications. His work has outcomes applied to security micro-kernels for high assurance systems like Electric-Vehicles and Spacecrafts, techniques for quantum computing verification and the certification of smart contracts. As a result, his research has been recognized by international standards like ARINC, and has been published in top tiers venues like CAV, FM, S&P, POPL, TDSC, and TOPLAS among others.

Publications

Journal Papers
  • Verification of Complex Dynamic Data Tree with Mu-Calculus, Maria del Mar Gallardo and David Sanan, Automated Software Engineering, 2013
  • An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model, Hou Zhe, David Sanan, Liu Yang, Chuen Hoa Koh, and Dong Jin Song, Journal of Automated Reasoning, 65:569 – 598, 2021
  • Pedro de la Camara, Maria del Mar Gallardo, Pedro Merino, and David Sanan. Checking the Reliability of Socket Based Communication Software. International Journal on Software Tools for Technology Transfer, 11:359 – 374, 2009
  • 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, 16(1):127 – 141, January 2019 -Maria del Mar Gallardo, Christophe Joubert, Pedro Merino, and David Sanan. A ModelExtraction Approach to Verifying Concurrent C Programs with CADP. Science of Computer Programming, 77(3):375 – 392, 2012
  • 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, 2020
  • Yongwang Zhao, David Sanan, Fuyuan Zhang, and Yang Liu. Formal Specification and Analysis of Partitioning Operating Systems by Integrating Ontology and Refinement.IEEE Transactions on Industrial Informatics, 12(4):1321 – 1331, August 2016
  • David Sanan, Zhao Yongwang, Lin Shang-Wei, and Yang Liu. CSim2 : Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee. ACM Transactions on Programming Languages and Systems, 43(1), February 2021
  • Maria del Mar Gallardo, Pedro Merino, and David Sanan. Model Checking Dynamic Memory Allocation in Operating Systems. Journal of Automated Reasoning, 42:229 – 264, 2009
  • Wilayat Khan, David Sanan, Zhe Hou, and Yang Liu. On embedding a hardware description language in Isabelle/HOL. Design Automation for embedded Systems, 2019.
Conference Papers
  • Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS, Yongwang Zhao and David Sanan, The 31st International Conference on Computer-Aided Verification, CAV, New York, US, July 2019
  • Xuan-Bach Le, David Sanan, Sun Jun, and Shang-Wei Lin. Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications. In International Conference on Engineering of Complex Computational Systems ICECCS 2020, Singapore, October 2020
  • Hou Zhe, David Sanan, Alwen Tiu, and Yang Liu. Proof Tactics for Assertions in Separation Logic. In The 8th International Conference on Interactive Theorem Proving, ITP, Brasilia, Brazil, September 2017
  • Ke Jiang, David Sanan, Yongwang Zhao, Shuanglong Kan, and Yang Liu. A Formally Verified Buddy Memory Allocation Model. In The 24th International Conference on Engineering of Complex Computer Systems, ICECCS, Guanzhou, China, November 201
  • Yongwang Zhao, Zhibin Yang, David Sanan, and Yang Liu. Based Formalization of Safety-Critical Operating Systems Standards - An Experience Report on ARINC-653 using EventB. In 26th IEEE International Symposium on Software Reliability Engineering, ISSRE, Gaithersburg, US, November 2015
  • Fuyuan Zhang, Yongwang Zhao, David Sanan, Yang Liu, Alwen Tiu, Shang-Wei Lin, and Jun Sun. Compositional Reasoning for Shared-variable Concurrent Programs. In The 22nd International Symposium on Formal Methods, FM, Oxford, UK, July 2018
  • Jiao Jiao, Shuanglong Kan, Shangwei-Lin, David Sanan, Yang Liu, and Jun Sun. Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity. In The 41st IEEE Symposium on Security and Privacy, San Francisco, USA, 2020
  • David Sanan, Yongwang Zhao, Hou Zhe, Fuyuan Zhan,Alwen Tiu, and Yang Liu. CSimpl: a Framework for the Verification of Concurrent Programs using Rely-Guarantee. In 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, Uppssala, Sweden, April 2017
  • Yongwang Zhao, David Sanan, Fuyuan Zhang, and Yang Liu. A Parametric Rely-guarantee Reasoning Framework for Concurrent Reactive Systems. In The 23rd International Symposium on Formal Methods, FM, Porto, Portugal, October 2019
  • David Sanan, Yang Liu, Yongwang Zhao, Zhenchang Xing, and Mike Hinchey. Verifying FreeRTOS’ Cyclic Doubly LInked List Implementation: From Abstract Specification to Machine Code. In The 20th International Conference on Engineering of Complex Computer Systems, ICECCS, Gold Coast, Australia, December 2015
  • Xuan-Bach Le, Shang-Wei Lin, Sun Jun, and David Sanan. Quantum Separation Logic: A Framework for Local Reasoning of Quantum Programs. In International Conference on Principles Of Programming Languages POPL 2022, Pennsylvania, January 2022
  • Shang-Wei Lin, Jun Sun, Hao Xiao, Yang Liu, David Sanan, and Henri Hansen. FiB: Squeezing Loop Invariants by Interpolation between Forward and Backward Reachability. InThe 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE, Urbana-Champaign, Illinois, USA, November 2017
  • Yu Zhang, Yongwang Zhao, David Sanan, Lei Qiao, and Jinkun Zhang. A Verified Specification of TLSF Memory Management Allocator using State Monads . In Symposium on Dependable Software Engineering Theories, Tools and Applications, SETTA 2019, Shanghai, China, November 2019
  • Hou Zhe, David Sanan, Alwen Tiu, Yang Liu, and Koh Chuen Hoa. An Executable Formalization of the SPARCv8 Instruction Set Architecture: A Case Study for the Leon3 Processor. In 21st International Symposium on Formal Methods, FM, Limassol, Cyprus, November 2016
Interests
  • Security micro-kernels
  • Smart Contracts Security
  • Quantum Computing
Education

  • PhD (Software Engineering)

    University of Malaga, Spain