Languages

Language-based Software Security

Our research aims at building a reliable and practical framework for developing trustable software systems. We will implement it based on the framework of Proof-Carrying Code(PCC).
Software safety means that the running of some software will not result in unacceptable risk, and usually includes type safety, control flow safety, and memory safety.
The goal of our first step is to prove that some errors, sush as typing errors, array accessing errors, nil dereference errors and memory leak, will be excluded from the generated code. That is, our safety policies will include both type safety and memory safety. We will focus on pointer safety(a kind of memory safety).
To achieve our goal, we have designed a C-like source language for programmers. It has pointer type and explicit memory management (alloc and free), while the calculus of pointers is forbidden. More details about the language will be found in the file of language definition. We have also designed an assertion language for the source language and a series of pointer logic (appendix) for reasoning about pointer assertions on the source language.
We are preparing for designing and implementing a compiler for this language. The compiler will

  • Generate verification conditions(VCs) for the program from the codes and assertions on them.
  • Translate the VCs into the representations of Coq (a kind of proof assistant), so programmers can write the proof of VC with the help of Coq tools. Programmers will use the rules in our pointer logic to prove the safety of the program. And the proof of VC will be used as another input of the compiler.
  • Compile source code into assembly code, while traslating VC and its proof into corresponding VC and proof in the assembly-level at the same time. So we have also designed an assembly-level proving system.
  • In the assembly-level proving system, proof will be checked and assembly codes will be extracted from the proof. And these codes, according to the proof, will respect to the safety policies.

 Now we have implemented some parts of the compiler, we will release source codes of the compiler when our testing work finished.

Documentation
 
Language Definitions

  • The PointerC Programming Language Specification (pdf)
     
  • Source-level Assertion Language (in Chinese) (pdf)
     
  • Assembly Programming Language (pdf) (doc)
     

Framework Definition

  • A Framework of Function-based Certified Assembly Programming. (pdf)

Technique Report

  • The Relations Between Separation Logic and the Pointer Logic. (pdf)

Examples

  • Pointer Logic Examples in Source-level
    • List (In Chinese) (pdf)
       
    • Doubly-linked List (In Chinese) (pdf)
       
    • Binary Tree (In Chinese) (pdf)
       
    • Balanced Binary-search Tree (In Chinese) (pdf)
  • Other Examples

Papers

  • A Pointer Logic for Verification of Pointer Programs. Yiyun Chen, Zhaopeng Li, Zhifang Wang, and Baojian Hua.  Chinese Journal of Software , Vol.21(No.3), pp.124-137, March 2010. [ bib |.pdf (Chinese Version) (English Version)
     
  • An Extension to Pointer Logic for Verification. Zhifang Wang, Yiyun Chen, Zhenming Wang, Wei Wang, and Bo Tian.  In Proceedings of 2nd IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), pages 49-56, Nanjing, China, Jun 2008. IEEE Computer Society. [ bib | .pdf ]
     
  • A Formal Certifying Framework for Assembly Programs. Zhaopeng Li, Yiyun Chen, Lin Ge, and Baojian Hua.  Chinese Journal of Computer Research and Development, 45(5):825-833, May 2008. [ bib | .pdf ]
     
  • An Assembly Pointer Logic: Design and Implementation. Zhaopeng Li, Yiyun Chen, Baojian Hua, Wang Wei, Tian Bo. Mini-Micro Systems. To appear. (In Chinese) (pdf)
     
  • Design and proof of a safe programming language PointerC. Baojian Hua, Yiyun Chen, Zhaopeng Li, Zhifang Wang, and Lin Ge.  Chinese Journal of Computers, 31(4):556-564, April 2008. [ bib | .pdf ]
     
  • A Pointer Logic for Safety Verification of Pointer Programs. Yiyun Chen, Baojian Hua, Lin Ge, Zhifang Wang. Chinese Journal of Computers. 31(3):372-380, March 2008. (pdf
     
  • Formal Description of Elementary Operations in Pointer Logic. Yiyun Chen. Technical Report. (pdf
     
  • Design of a Certifying Compiler Supporting the Proof of Program Safety. Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu. 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007). pp 117-126. IEEE Computer Society. June, 2007. (pdf)
     
  • A Pointer Logic and Certifying Compiler. Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu, and Zhifang Wang. Frontiers of Computer Science in China, 1(3):297-312, Jul 2007. [ bib | .pdf ] 
     
  • An Implementation of a Certifying Compiler Prototype. Cheng Liu, Yiyun Chen, Lin Ge, Baojian Hua. Computer Engineering and Applications. Volume 43, Number 21, pp 99-102. July 2007. (In Chinese) (pdf
     
  • A Pointer Logic and Certifying Compiler. Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu. Frontiers of Computer Science in China. 1(3), pp 297-312. August 2007. (pdf
     
  • Formal Specifications and Proof Methods for Object Code. Zhaopeng Li, Yiyun Chen, Lin Ge, Baojian Hua. Submitted for Publication. (pdf) 
     
  • Automatic Generation of Formal Specifications in Assembly Code Certification. Lin Ge, Yiyun Chen, Baojian Hua, Zhaopeng Li, Cheng Liu. Mini-Micro Systems. To appear. (In Chinese) (pdf)

Drafts

  • A Pointer Logic Dealing with Uncertain Equality of Pointers (Chinese Version).
    Hongjin Liang, Yu Zhang, Yiyun Chen, Zhaopeng Li, Baojian Hua. Feb, 2009. (pdf)  
  • An Example of Reasoning in Extended Pointer Logic: AIO Remove Request Function in Glibc.
    Hongjin Liang, Yu Zhang, Yiyun Chen, Zhaopeng Li, Baojian Hua. Feb, 2009. (pdf
  • A Pointer Logic for Verification of Pointer Programs.
    Zhaopeng Li,Yiyun Chen, Baojian Hua, Zhifang Wang. Accepted by Sixth Asian Workshop on Foundations of Software (AWFS'09), Tokyo, Japan, April 6-8, 2009. (pdf
     
  • A Pointer Logic for Verification of Pointer Programs(Extended Version).
    Zhaopeng Li, Yiyun Chen, Baojian Hua, Zhifang Wang. To appear. April, 2009. (pdf)

Talks

  • Research on Language-based Software Safety (pdf) (ppt)
     
  • Compiling and Making Proof for Program Safety (in Chinese) (pdf) (ppt)
     
  • A Pointer Logic and A Certifying Compiler (ppt)
     
  • The idea of proving pointer logic is not weaker than separation logic (in Chinese) (ppt)

Software
Proving System Prototype

Proof Examples

Soundness Proof

Pointer Logic Verification System

  • Coq implementation of the core part of the redesigned pointer logic (Source Code)
     

Certifying Compiler

  • The PLCC certifying compiler version 2.0 to be released. (Source Code)