3 ms·

I thought Ada did only runtime checks? I am asking for (and my template hackery implements) compile-time checks. Runtime checks are slow and don't fully mitigat

by kentonv 10y ago

I thought Ada did only runtime checks? I am asking for (and my template hackery implements) compile-time checks. Runtime checks are slow and don't fully mitigate security bugs, though they probably downgrade the bugs to DoS attacks. But if these are actually checked by the compiler, that's pretty cool and I might actually have to play with Ada at some point!

jackmott 10y ago
Idris or F*? I think they are not practical because compile times end up extremely slow. I think want you want will necessarily have this effect of very slow compile times.
- indolering 10y ago
  Came here to suggest Idris, as it compiles to C. F* is still experimental and Idris is just coming up on a RC. They could also drop down into C and manually verify it.
DannyBee 10y ago
First, generalized static invariants that are either correct all the time or computable all the time are, impossible, of course. Even of the simple form you are trying. Second, Ada 2012 has static type invariants (enforced at compile time) and dynamic type invariants (enforced at runtime) You should be able to do, at the very least, what you are doing, in a much simpler way. Plus, it has procedure level pre and post conditions that are checked In any case, the tools ADA has allows it to go further than what you want, actually. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) There is a formally verifiable language that is just a subset of ada (IE compilable as normal ada) but can formally verify what you want here even if static predicates can't. (Now all of the above said, i'm not sure i'd go this route, but yeah)
nickpsecurity 10y ago
Ada does a mix of both compile-time and run-time checks. It was systematically designed to eliminate errors in most parts of the development process as the book below shows. SPARK, an Ada variant, can prove absence of all kinds of errors in code with automated provers. Since Ada supports cross-language programming, the typical route is to do most of the key logic in Ada, anything static/simple in SPARK, and anything platform-related in native language if too hard to do in Ada. They periodically update them with recent versions at 2012 for Ada and 2014 for SPARK. http://www.adacore.com/uploads_gems/Ada_Safe_and_Secure_Booklet.pdf http://www.adacore.com/uploads_gems/Ada_Safe_and_Secure_Book... Note: See table of contents especially. http://cowlark.com/2014-04-27-ada/index.html http://cowlark.com/2014-04-27-ada/index.html Note: This "random walk through Ada" has a nice summary of all kinds of features it has from perspective of an outsider instead of an Ada developer. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) http://www.adacore.com/uploads/technical-papers/SPARKSkein_SBMF.pdf http://www.adacore.com/uploads/technical-papers/SPARKSkein_S... Note: Link to SPARK and an example by Rod Chapman on doing Skein in it. Just converting it from C to SPARK found an error in original code. Because of course it did haha...

by kentonv 10y ago

jackmott 10y ago

Idris or F*? I think they are not practical because compile times end up extremely slow. I think want you want will necessarily have this effect of very slow compile times.

indolering 10y ago
Came here to suggest Idris, as it compiles to C. F* is still experimental and Idris is just coming up on a RC. They could also drop down into C and manually verify it.

DannyBee 10y ago

First, generalized static invariants that are either correct all the time or computable all the time are, impossible, of course. Even of the simple form you are trying. Second, Ada 2012 has static type invariants (enforced at compile time) and dynamic type invariants (enforced at runtime) You should be able to do, at the very least, what you are doing, in a much simpler way. Plus, it has procedure level pre and post conditions that are checked In any case, the tools ADA has allows it to go further than what you want, actually. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) There is a formally verifiable language that is just a subset of ada (IE compilable as normal ada) but can formally verify what you want here even if static predicates can't. (Now all of the above said, i'm not sure i'd go this route, but yeah)

nickpsecurity 10y ago

Ada does a mix of both compile-time and run-time checks. It was systematically designed to eliminate errors in most parts of the development process as the book below shows. SPARK, an Ada variant, can prove absence of all kinds of errors in code with automated provers. Since Ada supports cross-language programming, the typical route is to do most of the key logic in Ada, anything static/simple in SPARK, and anything platform-related in native language if too hard to do in Ada. They periodically update them with recent versions at 2012 for Ada and 2014 for SPARK. http://www.adacore.com/uploads_gems/Ada_Safe_and_Secure_Booklet.pdf http://www.adacore.com/uploads_gems/Ada_Safe_and_Secure_Book... Note: See table of contents especially. http://cowlark.com/2014-04-27-ada/index.html http://cowlark.com/2014-04-27-ada/index.html Note: This "random walk through Ada" has a nice summary of all kinds of features it has from perspective of an outsider instead of an Ada developer. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) http://www.adacore.com/uploads/technical-papers/SPARKSkein_SBMF.pdf http://www.adacore.com/uploads/technical-papers/SPARKSkein_S... Note: Link to SPARK and an example by Rod Chapman on doing Skein in it. Just converting it from C to SPARK found an error in original code. Because of course it did haha...