Qazrw70uukxtafyahte0
SkillsCast

Authenticated Data Structures, Generically, in Haskell

11th October 2018 in London at CodeNode

There are 38 other SkillsCasts available from Haskell eXchange 2018

Please log in to watch this conference skillscast.

Https s3.amazonaws.com prod.tracker2 resource 41088130 skillsmatter conference skillscast o9nohu

"An authenticated data structure (ADS) is a data structure whose operations can be carried out by an untrusted prover, the results of which a verifier can efficiently check as authentic." (Andrew Miller et al.)

The most prominent example of such data structures is Merkle Trees, famously used in the Bitcoin protocol. Merkle Trees allow "lightweight clients" (verifier) to query "full nodes" (prover) about transactions contained in blocks without having to store all block data by themselves.

Andrew Miller et al. published a paper titled "Authenticated Data Structures, Generically" in Proceedings of the ACM Conference on Principles of Programming Languages (POPL), January 2014, where they show how a modified OCaml compiler can equip a wide variety of functional data structures automatically and generically with ADS capabilities - the same piece of OCaml source code is compiled into two different binaries, one version for the prover, one for the verifier. (http://soc1024.ece.illinois.edu/gpads/)

During this talk, you will learn how the same idea can be implemented in a lightweight way as a Haskell library (without the need for a modified compiler): Lars will introduce an abstract monad AuthM (together with a corresponding monad transformer AuthT), that comes with two interpreters, allowing two different interpretations of the same monadic code, one for the prover, one for the verifier.

The running example from the paper, a simple binary tree with authenticated lookup, can easily be implemented in AuthM.

The approach is flexible enough to allow for more sophisticated structures like balanced trees with authenticated insert, delete and lookup.

This is a nice case study of the use of different interpreters for a free monad and should appeal to a wider audience, not just those interested in ADS's.

The code can be found on GitHub.

YOU MAY ALSO LIKE:

Thanks to our sponsors

Authenticated Data Structures, Generically, in Haskell

Lars Brünjes

Lars is a pure mathematician by training, and holds a PhD in the same. He has spent several years teaching and doing postgraduate research in arithmetic number theory at Cambridge University in the UK, and at Regensburg University in Germany. He worked for ten years as a Lead Software Architect for an international IT company. His job, amongst other things, was the application of mathematical optimization techniques to the paper industry and web framework development (using mostly C#, JavaScript and TypeScript). His present position is that of Director of Education at Input Output Hong Kong (IOHK), working on blockchain technology and teaching Haskell and other subjects. He has been interested in programming since his early teens, and he loves learning new programming languages and paradigms - in particular those that offer a radically new way of looking at problems and of thinking about solutions. He is especially fascinated by functional programming and its promise of elegant, bug-free code that can be developed rapidly.

SkillsCast

Please log in to watch this conference skillscast.

Https s3.amazonaws.com prod.tracker2 resource 41088130 skillsmatter conference skillscast o9nohu

"An authenticated data structure (ADS) is a data structure whose operations can be carried out by an untrusted prover, the results of which a verifier can efficiently check as authentic." (Andrew Miller et al.)

The most prominent example of such data structures is Merkle Trees, famously used in the Bitcoin protocol. Merkle Trees allow "lightweight clients" (verifier) to query "full nodes" (prover) about transactions contained in blocks without having to store all block data by themselves.

Andrew Miller et al. published a paper titled "Authenticated Data Structures, Generically" in Proceedings of the ACM Conference on Principles of Programming Languages (POPL), January 2014, where they show how a modified OCaml compiler can equip a wide variety of functional data structures automatically and generically with ADS capabilities - the same piece of OCaml source code is compiled into two different binaries, one version for the prover, one for the verifier. (http://soc1024.ece.illinois.edu/gpads/)

During this talk, you will learn how the same idea can be implemented in a lightweight way as a Haskell library (without the need for a modified compiler): Lars will introduce an abstract monad AuthM (together with a corresponding monad transformer AuthT), that comes with two interpreters, allowing two different interpretations of the same monadic code, one for the prover, one for the verifier.

The running example from the paper, a simple binary tree with authenticated lookup, can easily be implemented in AuthM.

The approach is flexible enough to allow for more sophisticated structures like balanced trees with authenticated insert, delete and lookup.

This is a nice case study of the use of different interpreters for a free monad and should appeal to a wider audience, not just those interested in ADS's.

The code can be found on GitHub.

YOU MAY ALSO LIKE:

Thanks to our sponsors

About the Speaker

Authenticated Data Structures, Generically, in Haskell

Lars Brünjes

Lars is a pure mathematician by training, and holds a PhD in the same. He has spent several years teaching and doing postgraduate research in arithmetic number theory at Cambridge University in the UK, and at Regensburg University in Germany. He worked for ten years as a Lead Software Architect for an international IT company. His job, amongst other things, was the application of mathematical optimization techniques to the paper industry and web framework development (using mostly C#, JavaScript and TypeScript). His present position is that of Director of Education at Input Output Hong Kong (IOHK), working on blockchain technology and teaching Haskell and other subjects. He has been interested in programming since his early teens, and he loves learning new programming languages and paradigms - in particular those that offer a radically new way of looking at problems and of thinking about solutions. He is especially fascinated by functional programming and its promise of elegant, bug-free code that can be developed rapidly.

Photos