mrash / fwknop

Single Packet Authorization > Port Knocking
http://www.cipherdyne.org/fwknop/
GNU General Public License v2.0
1.09k stars 228 forks source link

Using the "C Bounded Model Checker" (CBMC) #364

Open mrash opened 7 months ago

mrash commented 7 months ago

Very strong validation of C code can be achieved through the usage of the C Bounded Model Checker (CBMC): https://www.cprover.org/cprover-manual/cbmc/tutorial/

The fwknop project should investigate its use in addition to all of the other security validation techniques it uses.