Dependent types

So, why are you not using dependent types yet? Do you like your programs randomly crashing?

>>80
people said the same thing about rust and go, but look what happened as a result

pretty much nothing

>>77
I'm just saying there's more to security than dependent types
many security issues aren't about language design
it's like saying access modifiers are the difference between a secure or insecure program lol

>>79
Please post about it.

>>81
Nobody said that about go and many supporters of dependent types raised their concerns when Rust appeared.

>>82
We are talking about software security here. Why are infosec people so dumb?

>>83
software security is more than just language design, a lot of it is what you do within the language

>>84
Yes, and dependent types filter out a lot of common errors when programming.

>>83

Please post about it.

It was mostly vidya logic, so not very /prog/ relevant. Shit like not realizing that bumping numbers without touching the underlying mechanics will just lead to more tedious kiting.

It's just that mentality of

I did something therefore it's fixed, thread over, issue closed, working as intended

that is impossible to work with. With those people, you have to convince them emotionally, by licking their asses and trying to sneak your ideas as theirs.

>>86
What project was that?

Bump

>>87
CDDA

>>89
The roguelike?

>>90
Yes

>>77
how the fuck do dependent types prevent priv-esc? do you even know what it is?

>>92

how the fuck do dependent types prevent priv-esc?

trivially

>>93

>>93
your're are an anus

>>93
if it's so trivial then explain it to me, anus

>>96
Give me an example and I will tell you how to prevent it with dependent types.

>>97
Prevent those dubs

Dubs

>>99
nice dubs

>>97
stop moving goalposts, anus. first you said that it can be trivially prevented, now you say that I must give you examples. this once again proves that your're are speaking out of your're are anus (recursively, because your're are an anus). but OK, I'll explain it to you:

priv-esc is not an attack method. it's a consequence of an attack: one user (normally a low-privileged one) can execute code as another (normally high-privileged). usually, it's done by exploiting a process running with desired privileges (so things like buffer overflows and injections, but also logic bugs and race conditions which cannot be trivially prevented by a type system), but it can also come from exploitation of bad OS-level configuration - e.g. parameter injection through shell expansion, world-writeable suid binaries/scripts, world-writeable (and overly powerful) configs etc. Edited on 22/11/2018 11:26.

>>97
stop moving goalposts, anus. first you said that it can be trivially prevented, now you say that I must give you examples. this once again proves that your're are speaking out of your're are anus (recursively, because your're are an anus) who doesn't know what he's talking about. but OK, I'll explain it to you:
stop moving goalposts, anus. first you said that it can be trivially prevented, now you say that I must give you examples. this once again proves that your're are speaking out of your're are anus (recursively, because your're are an anus). but OK, I'll explain it to you:

priv-esc is not an attack method. it's a consequence of an attack: one user (normally a low-privileged one) can execute code as another (normally high-privileged). usually, it's done by exploiting a process running with desired privileges (so things like buffer overflows and injections, but also logic bugs and race conditions which cannot be trivially prevented by a type system), but it can also come from exploitation of bad OS-level configuration - e.g. parameter injection through shell expansion, world-writeable suid binaries/scripts, world-writeable (and overly powerful) configs etc.

>>101

buffer overflows and injections

Can be prevented by dependent types.

but also logic bugs

Can also be prevented by dependent types.

and race conditions

You probably need linear types for that.

>>102
buffer overflows and injections can be prevented by dependent types (although it's harder for injections as they usually happen on the boundaries of languages - e.g. calling shell from C or SQL from PHP). logic bugs only theoretically can, but that's equivalent to formally proving a program - which is never trivial and can't be done in general case (because of halting problem).

of course you conveniently ignored how priv-esc can happen by exploiting OS-level stuff. lets see these guys implement diff dependent types prevent that

>>103

although it's harder for injections as they usually happen on the boundaries of languages

You could have a dependent type like system : (s : string) -> doesNotContainUnescapedQuotes s = True -> IO ()

logic bugs only theoretically can

Buffer overflows are also logic bugs.

can't be done in general case (because of halting problem).

Nice meme

by exploiting OS-level stuff

Dependent types can't prevent bugs in other programs.

>>104

doesNotContainUnescapedQuotes

that might be the only way to prevent shell injection but it's an anus-backwards approach when it comes to SQLi. the correct solution is not treating SQL queries as strings. see: parametrized queries.

Buffer overflows are also logic bugs.

buffer overflows aren't really what security people would call logic bugs. this term refers to unintended consequences of a program's high-level design, not low-level details about programming language, calling convention and the processor architecture.

Nice meme

dependent types solve halting problem?

Dependent types can't prevent bugs in other programs.

how would they prevent those bugs if an OS was written in a dependently typed language? that's a clear example of what I mean by 'logic bugs'

>>105

dependent types solve halting problem?

Languages with dependent types tend to not be Turing complete. Moreover the halting problem is irrelevant for just about anything.

how would they prevent those bugs if an OS was written in a dependently typed language?

Formal verification

>>106

Languages with dependent types tend to not be Turing complete.

lets see these guys implement diff a kernel

Formal verification

which is non-trivial, time-intensive and doesn't even require dependent types. you can look at any bug and say '100k additional man-hours by guys with PhDs would have prevent it', but that's not saying much.

meme