Related publications: [BS25]
Detecting flaws in SMTP implementations can be very difficult, because the underlying specification has grown extensively over multiple decades. We address this challenge with a cross- checking approach. Using active automata learning, we infer formal models of two different SMTP implementations (Postfix and Haraka). We then perform an automated comparison of these models to identify behavioural differences between the implementations. Finally, we perform a targeted inspection against the corresponding parts of the specification. Using this approach, we uncover multiple violations of the specification and some instances of unexpected behaviour. Furthermore, this work contributes a reusable method for cross-checking SMTP implementations, without requiring access to source code or formalised specifications. [BS25].