mastodon.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
The original server operated by the Mastodon gGmbH non-profit

Administered by:

Server stats:

348K
active users

The "robustness principle" is the most destructive concept in protocol design and implementation of all time. We should be embracing its inverse: strict, explicit state-machines with model-checked proofs

@hannesm @djm We did something like this for IKEv2 with TKM, which is part of strongSwan. (Library) Code generator which includes FSM and SPARK proof aspects for state transitions.

codelabs.ch/tkm/

@senier et al (now at AdaCore) has done a project called RecordFlux, which does much more: you can specify the protocol in a DSL and the tools will generate SPARK code with some formal guarantees. NVIDIA has actually used it in production.
Also, the code is opensource and up on GitHub.

codelabs.chTKMTrusted Key Manager in Ada
Kensan
arXiv.orgRecordFlux: Formal Message Specification and Generation of Verifiable Binary ParsersVarious vulnerabilities have been found in message parsers of protocol implementations in the past. Even highly sensitive software components like TLS libraries are affected regularly. Resulting issues range from denial-of-service attacks to the extraction of sensitive information. The complexity of protocols and imprecise specifications in natural language are the core reasons for subtle bugs in implementations, which are hard to find. The lack of precise specifications impedes formal verification. In this paper, we propose a model and a corresponding domain-specific language to formally specify message formats of existing real-world binary protocols. A unique feature of the model is the capability to define invariants, which specify relations and dependencies between message fields. Furthermore, the model allows defining the relation of messages between different protocol layers and thus ensures correct interpretation of payload data. We present a technique to derive verifiable parsers based on the model, generate efficient code for their implementation, and automatically prove the absence of runtime errors. Examples of parser specifications for Ethernet and TLS demonstrate the applicability of our approach.

@Kensan @hannesm @djm @senier I did network protocols in OCaml and it feels the same I guess. Except you have a garbage collector.

@thodg which network protocols did you do in OCaml? open source? :)

@hannesm no, very simple protocols, nothing fancy but it worked without a flaw everytime for a long time