The homepage of
Jonathan Hyldgård Samsing
I am studying for my MSc. in Computer Science at Aarhus University. Currently, I'm studying systems security, cryptologic protocol theory, as well as language-based security. For my Bachelor's I did a project concerning Bulletproofs and their implementation, as well as formal verification thereof.
You are reading a probabilistic website - what you see now may not be the same as what presents itself to another reader! If you are curious, try reloading the website. :-)
Projects
You may be able to find these projects on my GitHub. If it is not on my GitHub, you can mail me for a copy of the source code.
High-Assurance Bulletproofs protocol implementation
Bulletproofs implemented using the Hax language, which is a subset of Rust that translates to various proof-oriented languages such as Rocq and F*. Having translated it, you are then able to immediately prove panic-freedom by running the generated code - a larger feat than you might think! Additionally, you may then use the code generated to formally verify your codebase. Writing software like this, you truly start to appreciate how susceptible to crashing all your software is.
For example, what do we do for vector-polynomial multiplication? Let's say we do an early return if we find a dimensional mismatch. Then we get nonsense results. Let's say we instead assert that all vectors are the same size: this violates the panic-freedom property, and our implementation is no longer very secure.
The solution is to provide a compile-time guarantee that all our vector-polynomials are well-formed. This is where Rust's type system shines - we can create a `const T: usize` type parameter for our vector-polynomial and say that all of the coefficients must be slices of this size. Constant expressions in Rust are required to be evaluable at compile-time, and therefore we know, at compile-time, exactly how large the vectors are going to be. This trick applies to all instances of this problem - including vector addition, dot products, and of course, vector-polynomials.
The project, apart from the formal verification part (which is a whole topic in itself), also included various advanced concepts in cryptography. Elliptic curves and Pedersen commitments are particularly relevant here, with Pedersen commitments being implemented using the other.
Pedersen commitments are an additively homomorphic commitment scheme. Let's say you add commitments to two scalars together. This yields the same result as if you commited to the sum of the two. This is a super useful property that lets us optimize the size of the proof quite a bit - and of course, smaller proofs mean less data to send over a potentially slow internet connection! There are many other nice properties of Pedersen commitments, among others computational binding, which make it useful for Bulletproofs.
Elliptic curves over prime fields are used because they enable us to easily compute numbers that, similar to the discrete logarithm problem, are hard to factor. In particular, we can define elliptic curve point addition, which yields that the points of an elliptic curve form a group. And when we have this group, we can use it to construct new points using scalar multiplication as well as point addition. As it turns out, factoring the addition of two points on an elliptic curve defined over a prime field is super hard! Therefore this forms a great basis for Pedersen commitments, and they can thus be implemented very easily. Concretely, we used Curve25519, an elliptic curve devised by D. J. Bernstein which has a nice Rust implementation.
The above is only a surface description of my Bachelor's project. If interested, I'd actually recommend reading the original Bulletproofs paper - it's quite easy to read!
Mandelbrot visualizer
Tiny little afternoon project I did in C. It allows you to explore the Mandelbrot set by clicking on the part you'd like to zoom in on, and right-clicking to zoom out again.
Particle simulator
A simulator for a closed system of particles with energy preservation (bar the floating point imprecisions). Another smaller project in C, this is one of those classic projects where you read a bunch of physics off of Wikipedia and then write it into code.
