Get in Touch

With David Miguel Sanan Baena

Name and email
CAPTCHA
This question is for testing whether or not you are a human visitor and to prevent automated spam submissions.
Assistant Professor

David Miguel Sanan Baena

PhD (Software Engineering), University of Malaga, Spain
Cluster:
Infocomm Technology
Email
LinkedIn
Google Scholar

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.

 

 

Education

  • PhD (Software Engineering)
    University of Malaga , Spain

Research Interests

  • Security micro-kernels

    Security micro-kernels, and in particular the concept of separation micro-kernels, are an essential component for high-assurance systems. Nowadays, Internet of Things devices and Electric Vehicles require higher levels of security, and it is necessary to guarantee that those systems have minimal exposition to attacks. I have a very strong interest in the notion of separation micro-kernel in two different aspects: enhancing the security of the micro-kernel and guaranteeing their security and functional correctness.

  • Smart Contracts Security

    The blockchain and cryptocurrencies are here to stay with us. Blockchain represents a very powerful technology with applications like smart contracts that are definitely changing how financial transactions are handled. However, with great power comes great responsibility, and exploits on the foundations of smart contracts have caused millionaire loss. My research in this area focuses on the development of precise semantics able to characterize smart contracts that help to ensure that smart contracts are not exploitable.

  • Quantum Computing

    Quantum Computation is bringing computer capacities to higher levels. However, the programming paradigm is very different to traditional computation and it is easy to write quantum programs that do not achieve the expected results. My current research includes a framework to check the correctness of quantum programs using separation logic to ensure that they can scale to large systems.

Journal Papers

  • Maria del Mar Gallardo and David Sanan. Verification of Complex Dynamic Data Tree with Mu-Calculus. Automated Software Engineering, 20(4):569 – 612, 2013

  • Hou Zhe, David Sanan, Liu Yang, Chuen Hoa Koh, and Dong Jin Song. An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model. 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.

Conferences

  • Yongwang Zhao and David Sanan. Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS. In 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