[FEATURE] Demo example of using CN to prevent memory error in real-world C code

[podhrmic]

Summary

The motivation for this example is to show a bottom-up spec writing approach. A programmer is writing some code that should do X, and has some notion of what the correct functionality should be (e.g. do some operation, or just avoid memory errors). Show how writing these specs would prevent a real-world CVE.

I looked at CVEs related to popular C network stacks, and picked the ones that seemed relevant, specifically:

• CVE-2020-22284 - buffer overflow vulnerability in lwip
• CVE-2020-22283 - buffer overflow vulnerability in lwip
• a number of various picotcp vulnerabilities (pick from the critical ones)
• a number of various FreeRTOS vulnerabilities - (pick from the critical ones)
  • this one could be interesting: STMicroelectronics/stm32-mw-usb-host@15c4631

Do

• an example is identified
• appropriate CN specs is written
• slides/readme about the example is available

[podhrmic]

Changed to Someday as this is not immediately needed for the August 13 demo