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;
}
The Verifiable C volume of Software Foundations deals with formally verifying C code in Coq. They also talk about malloc and free here. 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. See this for the proofs.