Blogs by Michiel

Tech blog on web, security & embedded
The Dutch Electoral Council (known as the Kiesraad in Dutch) are developing Abacus: new open-source software for computing election results. We looked into how we can verify the correctness of the algorithm used for seat apportionment. In this blog post, we will discuss various ways of verifying software in Rust, from unit testing to model-based verification and fuzzing. In particular, property-based fuzzing turned out to be very useful for finding bugs in the seat apportionment algorithm.
Java is one of the most commonly used programming languages that we have not yet discussed in our Rust Interop Guide. In this article, we will discuss three different methods to call Rust code from Java: JNI, JNR-FFI and Project Panama. We will show the differences between these methods and we will do some basic benchmarking to compare their performance. These methods not only work for Java but also for other JVM languages like Kotlin. Here we will mainly focus on Java, but Kotlin examples are available in the Kotlin branch of our GitHub repository.

The NTP protocol is used by many devices to synchronize their system clocks. However, many devices use SNTP clients (Simple NTP) which are even more vulnerable to interference. As most (S)NTP packets are unauthenticated, they are vulnerable to spoofing, making it possible to change a device's time by manipulating (S)NTP packets.

In this blog, we discuss how (S)NTP packets can be forged to manipulate a device's system clock. Especially on the default SNTP client for many Linux systems, this turned out to be very easy. We will also discuss the consequences of such attacks, as well as how these attacks can be prevented.