I am interested in dependent type systems, total languages, and similar methods of proving certain program errors cannot occur, although I would have to do some background research to learn more of the state of the art in that field.
If you’re not already familiar with Idris, I highly recommend checking it out—it’s a dependently typed Haskell variant, a bit like Agda but with a much friendlier type syntax. The downside of Idris is that, as a newer language, it doesn’t have nearly as robust a standard library of proofs as, say, Coq. That said, the author, Edwin Brady, is keenly focused on making it a good language for expressing security properties in.
The field I work in has to do with proving that program errors related to maliciously crafted input cannot occur; if it’d be useful I’m happy to braindump/linkdump.
I’d heard of Idris. Parts of it sound really good (dependent typing, totality, a proper effects system, being usable from Vim), although I’m not a huge fan of tactic-based proofs (that’s what the Curry-Howard Isomorphism is for!). It’s definitely on the top of my list of languages to learn. I wasn’t aware of the security focus, that is certainly interesting.
Proving safety in the face of malicious input sounds fascinating—a dump would be much appreciated.
I have not actually learned Idris yet, and I think I could motivate myself better if I had a study partner; would you be interested in something like that?
Depends mainly on how we both learn best. For me, when it comes to learning a new language that tends to be finding a well-defined, small (but larger than toy) project and implementing it, and having someone to rubber-duck with (over IM/IRC/email is fine) when I hit conceptual walls. I’m certainly up for tackling something that would help out MIRI.
Also, presuming that the talk Andreas Bogk has proposed for 30c3 is accepted, you’ll want to see it—it’s a huge pragmatic leap forward. (I apologize for not being at liberty to go into any more detail than that. The talk will be livestreamed and recorded, FWIW.)
If you’re not already familiar with Idris, I highly recommend checking it out—it’s a dependently typed Haskell variant, a bit like Agda but with a much friendlier type syntax. The downside of Idris is that, as a newer language, it doesn’t have nearly as robust a standard library of proofs as, say, Coq. That said, the author, Edwin Brady, is keenly focused on making it a good language for expressing security properties in.
The field I work in has to do with proving that program errors related to maliciously crafted input cannot occur; if it’d be useful I’m happy to braindump/linkdump.
I’d heard of Idris. Parts of it sound really good (dependent typing, totality, a proper effects system, being usable from Vim), although I’m not a huge fan of tactic-based proofs (that’s what the Curry-Howard Isomorphism is for!). It’s definitely on the top of my list of languages to learn. I wasn’t aware of the security focus, that is certainly interesting.
Proving safety in the face of malicious input sounds fascinating—a dump would be much appreciated.
“Security Applications of Formal Language Theory” is a good overview. (If you don’t have IEEE access, there’s a tech report version.) Much of the work going on in this area has to do with characterizing classes of vulnerabilities in terms of unintended computational automata that arise from the composition of independent systems, often through novel vulnerability discovery motivated by considering the formal characteristics of a composed system and figuring out what can be wedged into the cracks. There’s also been some interesting defensive work (Haskell implementation, an approach I’m interested in generalizing). That’s probably a good start.
I have not actually learned Idris yet, and I think I could motivate myself better if I had a study partner; would you be interested in something like that?
I might be interested in being your study partner; what would that involve?
Depends mainly on how we both learn best. For me, when it comes to learning a new language that tends to be finding a well-defined, small (but larger than toy) project and implementing it, and having someone to rubber-duck with (over IM/IRC/email is fine) when I hit conceptual walls. I’m certainly up for tackling something that would help out MIRI.
Sounds like fun! I’ll PM you my contact details.
What do you mean by having a study partner?
Also, presuming that the talk Andreas Bogk has proposed for 30c3 is accepted, you’ll want to see it—it’s a huge pragmatic leap forward. (I apologize for not being at liberty to go into any more detail than that. The talk will be livestreamed and recorded, FWIW.)