Generally, during fuzz testing (regardless of the tool used to perform it: American Fuzzy Lop, libFuzzer, or any other), we have to remember to keep the number of iterations per second high. This means that a good fuzzer is a fast fuzzer. This is mostly facilitated by minimizing the structures and operations needed to prepare the context. We do not reinitialize the mechanisms of the fuzzed library for every iteration.

Fuzzing is a software testing method that involves passing malformed data as input to the program and monitoring it for misbehavior. Today, fuzzing is one of the most effective ways to find software security problems. In 2014, Michał Zalewski presented American Fuzzy Lop, the first coverage guided fuzzer. This started the modern world of fuzzing solutions and techniques on the market.

Continuing from our previous article, let us take an example of how to write a TLA+ proof for a real-world specification of a distributed system. For this exercise we will go through the Voucher Trading System process as specified by the RFC3506 hosted by IETF. The distributed and concurrent systems require a consensus protocol to achieve overall system reliability and immunity to failures of nodes. We decided to select for this VTS network a simple Two-phase commit protocol.

When engineers were designing completely autonomously operated Paris Métro line 14, they had to ensure the safety of tens of millions passengers each year, its 22 stations across Paris as well as smooth running of trains. How to approach development of software that allows for the automation of public transit? The French team decided to use formal verification – learn what it means!

Userland Toolchain Sanitizers, Hardened Allocators. Stack Hardening. Expertise in modern security-oriented and coverage-aided fuzzers for kernels, libraries and applications. Kernel ASLR, Kernel Sanitizers, CPU Bugs Mitigation, Network Stack Hardening, Software and Hardware Assisted Virtualization, Device Driver Fuzzers.