From 569b689dd557a17d94c965d47a092379cec69456 Mon Sep 17 00:00:00 2001 From: Jonathan Anderson Date: Fri, 21 Jun 2013 10:45:21 +0100 Subject: [PATCH] Things that people agreed to do with TESLA. --- plans.txt | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 plans.txt diff --git a/plans.txt b/plans.txt new file mode 100644 index 0000000..fe3830e --- /dev/null +++ b/plans.txt @@ -0,0 +1,38 @@ +Things people are going to look at: +* rwatson + * socket lock verification +* kg365 + * MAC framework ( + audit?) + * OpenSSH (sshd) +* theraven + * Python Objective-C bindings ("spectacularly shoddy code") + * cross-language assertions (e.g. Smalltalk) -> requires dynamic registration + * Xlib/Xcb: some X state-machine checking already +* marinosi + * marinosi's stack +* avsm2 + * OCaml GC (C interface) +* bz + * possibly ND6 or IPSEC assertions? +* jon + * check ability to express BigKnife's state machines + * will ponder Capsicum +* brooks + * dhclient + * will ponder Capsicum + + +Other possible targets: +* OpenSSL + * how many ports do it wrongly? +* Kerberos +* Kernel TCP? +* John Baldwin's thread, process state machines +* Xen? (split drivers, etc.) +* PAM ("complex, annoying, stateful")? +* NFSv4? + * nfslockd +* PPP + * lots of handcrafted switch cases +* named, libresolve +