|
|
|
|
|
|
by touisteur
1440 days ago
|
|
|
I feel this would be a good place to use a spark-based TCP stack. You're bypassing the kernel, have to run stuff as root or risky CAP_ rights, your stack should be as solid as possible. https://www.adacore.com/papers/layered-formal-verification-o... Might also give people here some ideas on how to combine symbolic execution, proof, C and SPARK code and how to gain confidence in each part of a network stack. I think there's even some ongoing work climbing up the stack up to HTTP but not sure of the plan (not involved). |
|
|