In my last post, I summarized some of the topics and problems considered at a recent Dagstuhl seminar I co-organized on the Synergy between Programming Languages and Cryptography. The post surveyed how programming languages often interface with cryptography in the construction of secure systems, and in particular how they can make it easier to implement cryptography, use it, or verify its correctness.
Beyond using PLs as a tool for easier/safer use of Crypto, there is an opportunity for certain kinds of thinking, or reasoning, to cross over fruitfully between the PL an Crypto communities. In particular, both communities are interested in formalizing systems and proving properties about them but they often use different methods, either due to cultural differences, or because the properties and systems of interest are simply different. During the workshop we identified both analogous, similar styles of reasoning in two communities and connection points between the different styles of reasoning. In this post I briefly highlight a few examples of each, and point to future research opportunities.
Continue reading →
Filed under Formal verification, Program Analysis, Secure computation, Semantics, Software Security, Uncategorized
Tagged as contextual equivalence, crypto currency, cryptography, differential privacy, formalism, full abstraction, garbled circuits, oblivious RAM, proof, real-ideal paradigm, secure multiparty computation
I recently had the pleasure of co-organizing a Dagstuhl Seminar on the synergy between ideas, methods, and research in programming languages and cryptography.
Dagstuhl Seminar on the Synergy between Programming Languages and Cryptography
This post and the next will summarize some interesting discussions from the seminar. In this post, I will look at how programming languages often interface with cryptography, surveying the research of the seminar participants. In my next post, I’ll dig a little deeper into one topic in particular, which is how formal reasoning in PL and Crypto compare and contrast, and how ideas from one area might be relevant to the other.
Ultimately, I came away convinced that the combination of PL and Crypto has much to offer to the problem of building secure systems.
Continue reading →
Filed under Formal verification, Research, Research directions, Secure computation, Software Security
Tagged as compilation, cryptography, MPC, proof, SNARK, Verification, zero knowledge