NewsPublication 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)
I am currently researching on verification applied to security for cyber-physical systems in the Securify project, which has been awarded with an NRF grant.
The Securify project aims to ensure security in the execution stack of cyber-physical systems. Securify applies verification by means of compositional techniques from the lower layers of the system, i.e., the hardware and micro-kernel, to the upper layers, verifying libraries and applications, and including the automatic generation of safe code. To improve security, Securify uses hardware and software techniques for the dynamic analysis of the code under analysis.
My main research line is the verification of the separation micro-kernel, 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 am currently working on the verification of the 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 play a team coordinator role.
Other research tasks I am involved within the Securify are formal verification of the Leon3 processor, a SPARC V8+ multi-core CPU and formalization of executable semantics for the RUST language for safe code generation, and the research of compositional techniques for verification scalability.
- 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)
- 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)
- 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
- 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
- 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
- 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).
- 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.
- 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
- 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
- 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
- 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
- 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.
- 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
- 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.
- 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.
- 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
- 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.
- 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
- PhD student at University of Málaga. From Dec 2004 to Nov 2009. Techniques for the Automatic Analysis of Software Described in Programming Languages
- 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.
- 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.
- Postdoc at Trinity College Dublin. From July 2012 to December 2013. Modelling and verification of a separation microkernel by means of theorem proving.
- Postdoc at National University of Singapore. From January 2014 to January 2015. Machine code verification by means of theorem proving.
Room No: B2-26, Block N4 School of Computer Science and Engineering, Nanyang Technological University 50 Nanyang Avenue, Singapore 639798
Email: sanan AT ntu.edu.sg