4 ms·

Can you estimate the complexity of applying this type system to the whole openssl code?

by ecesena 12y ago

tomp 12y ago
In theory, it would be quite complex, as is every refactoring of existing code. I imagine that if all the primitive functions (e.g. memcpy, malloc, etc.) would be annotated with contracts, the system could pinpoint all the places that need proof. However, most functions would need annotations; refined type inference would help with this (like [1], [2] and [3]), but I'm not sure it's advanced enough already. In practice, this experiment isn't powerful enough for this. To support C, the refined type-checker would have to know how to reason about mutable state, and unless pointers are severely restricted, they would always enable an escape hatch (for the sloppy or rogue programmer). Projects that would help are Cyclone (an attempt at memory-safe C), Rust and VCC [4] (which, however, is focused at concurrency). Altogether, it would be much easier to start with a safer language and design for memory safety and/or verified contracts from the ground up.
- pascal_cuoq 12y ago
  So if I understand correctly, your system can prevent Heartbleed, except that it cannot analyze OpenSSL as written and that Heartbleed is a specific OpenSSL vulnerability. Does your system prevent Ariane 5 from exploding too?
  - tomp 12y ago
    I can't change the past, I can only change the future.
    - pascal_cuoq 12y ago
      I hate to be the one to break it to you, but you did not invent the idea of reducing the good behavior of programs to first-order logic properties and to apply an SMT solver to these. You are not even at the point where you might compare your false-positive rate to their false-positive rate, but if someone was going to change the future with that idea, the future of 20 years ago would have been changed. And perhaps it was. But if SPARK83, to take one system amongst others, did not prevent Heartbleed, I don't see how your system “can prevent Heartbleed”. It can't, because Heartbleed is not written in the language at https://github.com/tomprimozic/type-systems/blob/master/refined_types/expr.ml#L75 https://github.com/tomprimozic/type-systems/blob/master/refi... Describing your github repository with the words “can prevent Heartbleed” is disingenuous and unscientific. You should keep the dramatic hyperbole for the grant proposals.
      - tomp 12y ago
        > you did not invent the idea of reducing the good behavior of programs to first-order logic properties and to apply an SMT solver to these I know, that's why I cited a bunch of them in the README file.

Can you estimate the complexity of applying this type system to the whole openssl code?

by ecesena 12y ago

Can you estimate the complexity of applying this type system to the whole openssl code?

tomp 12y ago

In theory, it would be quite complex, as is every refactoring of existing code. I imagine that if all the primitive functions (e.g. memcpy, malloc, etc.) would be annotated with contracts, the system could pinpoint all the places that need proof. However, most functions would need annotations; refined type inference would help with this (like [1], [2] and [3]), but I'm not sure it's advanced enough already. In practice, this experiment isn't powerful enough for this. To support C, the refined type-checker would have to know how to reason about mutable state, and unless pointers are severely restricted, they would always enable an escape hatch (for the sloppy or rogue programmer). Projects that would help are Cyclone (an attempt at memory-safe C), Rust and VCC [4] (which, however, is focused at concurrency). Altogether, it would be much easier to start with a safer language and design for memory safety and/or verified contracts from the ground up.

pascal_cuoq 12y ago
So if I understand correctly, your system can prevent Heartbleed, except that it cannot analyze OpenSSL as written and that Heartbleed is a specific OpenSSL vulnerability. Does your system prevent Ariane 5 from exploding too?
- tomp 12y ago
  I can't change the past, I can only change the future.
  - pascal_cuoq 12y ago
    I hate to be the one to break it to you, but you did not invent the idea of reducing the good behavior of programs to first-order logic properties and to apply an SMT solver to these. You are not even at the point where you might compare your false-positive rate to their false-positive rate, but if someone was going to change the future with that idea, the future of 20 years ago would have been changed. And perhaps it was. But if SPARK83, to take one system amongst others, did not prevent Heartbleed, I don't see how your system “can prevent Heartbleed”. It can't, because Heartbleed is not written in the language at https://github.com/tomprimozic/type-systems/blob/master/refined_types/expr.ml#L75 https://github.com/tomprimozic/type-systems/blob/master/refi... Describing your github repository with the words “can prevent Heartbleed” is disingenuous and unscientific. You should keep the dramatic hyperbole for the grant proposals.
    - tomp 12y ago
      > you did not invent the idea of reducing the good behavior of programs to first-order logic properties and to apply an SMT solver to these I know, that's why I cited a bunch of them in the README file.