[langsec-discuss] state machine attacks against TLS (SMACKTLS)
munin at mimisbrunnr.net
Thu Mar 5 23:31:33 UTC 2015
This is, to the best of my knowledge, what miTLS already does, except
for them their state machine is formally encoded at the type layer of
their TLS implementation using F7
(http://research.microsoft.com/en-us/projects/f7/). This is also, to
the best of my knowledge, how these issues were discovered in TLS in
the first place.
Different process calculus's have been available for a while (the
seventies) to formally model the state and interaction between
concurrent communicating systems and some work
overview) has been done on encoding the rules of these systems into a
type system. There the idea would be that if you write your program
where the type system specifies the interactions between parties, if
the specification is correct, then the implementation is correct.
Refinement/session types seem to have real value in that they let us
find these weird errors in complicated and real world protocols. If
only more people used them...
On 03/05/2015 06:22 PM, travis+ml-langsec at subspacefield.org wrote:
> So, I haven't looked at the JSSE (that is, JDK) implementation of
> TLS, but I'm guessing that based on the number of erroneous
> transitions, they implemented an ad-hoc state machine interwoven
> with the code rather than modeling the FSM abstractly with explicit
> calls to make transitions. I am sure this sounds familiar to the
> readers of this list, as the state machine is the state of the
> network data parser.
> My intuition tells me that a large number of protocols could be
> handled in a much safer by encoding a formal FSM with named
> transitions that are explicitly invoked from the software and
> which throw exceptions back if the transition is not allowed.
> Further by decoupling the FSM & associated client state from the
> software it should be much easier to drive multiple state machines
> at once with a single network daemon*.
> If you were to do that you might be able to factor the parser out
> (possible also for formal treatment) and have a single daemon
> handling multiple services for multiple clients (a la inetd and the
> old stateless services it handled directly). One could then
> potentially limit resource consumption for a single client across
> services to prevent resource consumption attacks. This was a
> bigger deal when I thought of it in the 90s; now most servers are
> [*] OS interactions such as assuming a given effective userid, or
> irrevocably dropping permissions would be difficult, but possible
> if one factored the "OS actor" out into its own component (each FSM
> would have exactly zero or one of these as appropriate for the
> service being handled).
> In the case of safe languages and frameworks (erlang?), one could
> run the protocol parser in a common memory space and avoid
> security (process) boundary transition overhead (e.g. IPC overhead,
> scheduler latency, TLB flush). Similarly the FSMs could be handled
> directly in the process space as well. In the case of the OS
> actor, that must necessarily be its own process context, but shared
> memory or zero-copy IPC like that used by L4 microkernel could
> reduce that overhead significantly. The entire ecosystem might be
> modelable as a message passing architecture.
> This idea's pieces have been sitting undone on my list here:
> Specifically, the 90s-influenced use cases:
> Write a network daemon in a "safer" language than C (java, perl,
> python, ML). See privilege.py for example of how to drop
> privileges safely.
> Write something like tcpdump or wireshark, but write the protocol
> decoding routines in a safer language. ruby and python come to
> mind, but ocaml might be faster.
> _______________________________________________ langsec-discuss
> mailing list langsec-discuss at mail.langsec.org
More information about the langsec-discuss