NewsPublication Accepted in CAV19. "Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS. Yongwang Zhao, 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.
- 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.
- Yongwang Zhao, 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, Liu Yang. 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
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