# Coq Prove code security

**URL:** <https://discourse.rocq-prover.org/t/coq-prove-code-security/1390>\
**Category:** Using Rocq\
**Tags:** software-foundations\
**Created:** [July 22, 2021, 11:50am UTC](https://discourse.rocq-prover.org/t/coq-prove-code-security/1390 "2021-07-22T11:50:33Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![niuzhi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/niuzhi/32/571_2.png) [@niuzhi](https://discourse.rocq-prover.org/u/niuzhi)\
**Post date:** [July 22, 2021, 11:50am UTC](https://discourse.rocq-prover.org/t/coq-prove-code-security/1390/1 "2021-07-22T11:50:33Z")

</div>

1.Recently, I am studying how to use Coq to prove the security of the code, and whether I can recommend some documents or materials. thank you very much.  
2.Does Coq have a plugin for translating source code into HOL?

for eample。Memory leak security issue。

#include \<stdio.h\>  
#include \<stdlib.h\>  
int main(){  
char _p = (char_)malloc(100 \* sizeof(char));  
p = (char\*)malloc(50 \* sizeof(char));  
free(p);  
p = NULL;  
return 0;  
}

---

<div class="post-metadata">

**Author:** ![siraben](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/siraben/32/528_2.png) [@siraben](https://discourse.rocq-prover.org/u/siraben)\
**Post date:** [July 26, 2021, 10:12am UTC](https://discourse.rocq-prover.org/t/coq-prove-code-security/1390/2 "2021-07-26T10:12:19Z")

</div>

The [Verifiable C volume](https://softwarefoundations.cis.upenn.edu/vc-current/toc.html) of Software Foundations deals with formally verifying C code in Coq. They also talk about malloc and free [here](https://softwarefoundations.cis.upenn.edu/vc-current/Verif_stack.html#lab45). In that program a possible direction to proceed is to assert that at the end of the program all the malloc tokens are freed, and the library will prevent you from proving that assertion because there would be a malloc token that is not freed.

An more realistic example of proving the correctness of operations on a binary search tree implemented [here](https://github.com/PrincetonUniversity/VST/blob/f78b26c277c9bb57f0db878602659e8552f6cdca/progs64/bst.c). See [this](https://github.com/PrincetonUniversity/VST/blob/f78b26c277c9bb57f0db878602659e8552f6cdca/progs64/verif_bst.v) for the proofs.