3 ms·

I could say exactly the same for Rust, that it's not enough even using unsafe keyword and I need to go into assembly. Someone could even say that assembly is no

by lossolo 10y ago

I could say exactly the same for Rust, that it's not enough even using unsafe keyword and I need to go into assembly. Someone could even say that assembly is not enough and we need FPGA and then ASIC etc. But it's not the point here. The point is that for ex. you can't get safety from out of bounds access without bound checking, doesn't matter which language you use. And bound checking for certain hot paths is not acceptable.

Manishearth 10y ago
> doesn't matter which language you use Idris.
- lossolo 10y ago
  Care to elaborate? I don't see how this can be done without trading space/time over solution without bound checking.
  - Manishearth 10y ago
    It won't work in all cases :) IIRC Idris will move type info to runtime if it can't prove it at compile time. Basically, in Idris I can have a function concat which takes a Vector<N, T>, a Vector<M,T>, and produces a Vector<N+M, T>. You can have arbitrary expressions there, and even things like a function which returns a different type based on its boolean argument. So most signatures will just carry dependencies through, but some things are dependent on runtime input and that's when the "N" part of the type will be tracked at runtime. At least, that's how I think it works. Dependent types help eliminate large swaths of bounds checks. Not all of them, and I'm not sure how much better it does than a good optimizing compiler.
    - lossolo 10y ago
      > I'm not sure how much better it does than a good optimizing compiler. It can be done by static analysis by compilers in other languages also. Knowing size at compile time is easy most of the time and we are not talking at all about this case. Your answer that Idris solves that is wrong in the context that this discussion started (dynamically allocated memory/not knowing the size compile time). You still need to trade time/space comparing to solution without bound checking, doesn't matter which language you use. I am getting info that I am submitting too fast? so answer to your other comment will need to wait.
      - Manishearth 10y ago
        Yes, it can be done by static analysis, but by making size dependencies part of the API it makes the static analysis much easier and able to cross API boundaries without needing to inline, on the contrary most optimizers will not handle such invariants across a few layers of function calls. Like I said, Idris doesn't solve this problem completely, but it is able to eliminate bounds checks in way more situations because the default is effectively no bounds checking. The nice thing about dependent types is that in all the cases where you don't need a bounds check -- where a program invariant enforces that you are within bounds -- your code will not contain a bounds check regardless of optimization. Only in the cases where there are runtime dependencies that can't be resolved will there be issues, and in thee cases you need a bounds check anyway. It's not perfect/complete, and like I said optimizers can get most of the way there anyway. I just wanted to note that there are better solutions for bounds checking.
naasking 10y ago
> And bound checking for certain hot paths is not acceptable. I think the history of exploits proves that it's always acceptable for server code. The only possibly justifiable place to omit bounds checking is isolated, high performance numerical code, as used in scientific simulations. But this code isn't exposed to the public, so its vulnerabilities aren't important.

by lossolo 10y ago

Manishearth 10y ago

> doesn't matter which language you use Idris.

lossolo 10y ago
Care to elaborate? I don't see how this can be done without trading space/time over solution without bound checking.
- Manishearth 10y ago
  It won't work in all cases :) IIRC Idris will move type info to runtime if it can't prove it at compile time. Basically, in Idris I can have a function concat which takes a Vector<N, T>, a Vector<M,T>, and produces a Vector<N+M, T>. You can have arbitrary expressions there, and even things like a function which returns a different type based on its boolean argument. So most signatures will just carry dependencies through, but some things are dependent on runtime input and that's when the "N" part of the type will be tracked at runtime. At least, that's how I think it works. Dependent types help eliminate large swaths of bounds checks. Not all of them, and I'm not sure how much better it does than a good optimizing compiler.
  - lossolo 10y ago
    > I'm not sure how much better it does than a good optimizing compiler. It can be done by static analysis by compilers in other languages also. Knowing size at compile time is easy most of the time and we are not talking at all about this case. Your answer that Idris solves that is wrong in the context that this discussion started (dynamically allocated memory/not knowing the size compile time). You still need to trade time/space comparing to solution without bound checking, doesn't matter which language you use. I am getting info that I am submitting too fast? so answer to your other comment will need to wait.
    - Manishearth 10y ago
      Yes, it can be done by static analysis, but by making size dependencies part of the API it makes the static analysis much easier and able to cross API boundaries without needing to inline, on the contrary most optimizers will not handle such invariants across a few layers of function calls. Like I said, Idris doesn't solve this problem completely, but it is able to eliminate bounds checks in way more situations because the default is effectively no bounds checking. The nice thing about dependent types is that in all the cases where you don't need a bounds check -- where a program invariant enforces that you are within bounds -- your code will not contain a bounds check regardless of optimization. Only in the cases where there are runtime dependencies that can't be resolved will there be issues, and in thee cases you need a bounds check anyway. It's not perfect/complete, and like I said optimizers can get most of the way there anyway. I just wanted to note that there are better solutions for bounds checking.

naasking 10y ago

> And bound checking for certain hot paths is not acceptable. I think the history of exploits proves that it's always acceptable for server code. The only possibly justifiable place to omit bounds checking is isolated, high performance numerical code, as used in scientific simulations. But this code isn't exposed to the public, so its vulnerabilities aren't important.