[2.0-scala] TLS client certificate auth design issue - partly verified claims

Here is an interesting Scala design issue for adding TLS client authentication to Play2.0 in a flexible manner. What is valid for Play2.0 is equally valid for unfiltered, or any other web framework, so I am sending this out a bit more widely.

Future[Seq[Certificate]]
========================

I recently put together a patched version of Play2.0.3 [1] which supports client authentication. This allows the client to request a certificate with a call to the certs method whose signature is:

  trait RequestHeader { ... def certs: Promise[Seq[Certificate]] ... }

 The reason it is a Promise (will be Future in Play 2.1), is because TLS renegotiation could take time - calling the method will open a client certificate selection box on the user's computer, and the user could take time to choose between one of his many certs. So we return a future immediately, and thereby avoid using up a thread (saving: 0.5MB of RAM)
   The use of promises/futures here is already a huge improvement over what Java frameworks do by default. But we can do better. 

   For those who are not so familiar with Certificate authentication, let me just fill in the reason we have a Seq[Certifictate]: this is because usually in Certificate Authority (CA) based authentication you get certificate chains, each Certificate being signed by the next. If you trust one of the CAs, then you can trust what the Certificate[0] says. The JVM allows you to set your Trust Store of CAs you trust, and usually all works out of the box from there.

   BUT this simplicity in operation is also the reason TLS authentication has not been widely adopted. The CA verifiction is simple but Big Brotherish: If you trust the CA (Big Brother) you can trust what the certificate says - but if forces everyone to go through a CA. The problem is it requires client certificates to be signed by CAs which few do properly, is expensive, tedious for the end user, inflexible, and in fact just plain impossible. It is just a very bad way of doing things. ( see the video on http://webid.info/ and many other explanations on my home page ).


Flexibility
===========

  What we need is something a lot more flexible - and yet still simple to use - playfully simple. So for example, we may want to be able to authenticate someone with or  without CA verification. What would that look like? Here are three levels one could distinguish.

 A. PublicKey Principal
 ----------------------

 Any TLS authentication verifies that the user has the private key of the public key sent by the 
certificate: so one can already use the public key of the certificate as an indirect identifier. 
This indirect identification is what the Principal class allows. One can extend it
and create a special subclass for this purpose

  case class PublicKeyPrincipal(pubKey: java.security.PublicKey) extends java.security.Principal

 This at least guarantees identity without the server needing to keep a password for the user, and it could work across sites. It does not guarantee anything else in the certificate is true. 

 B. WebID principal
 ------------------

  If there are SubjectAlternativeNames in the X509 certificate, one can use those URLs as global ids for the user. If the certificate is not signed by a CA one trusts one can follow the procedure outlines on the W3C WebID specification proposal ( http://webid.info/spec/ ) to verify that the WebID does indeed refer to the person who sent the certificate. When verified one would end up with a very useful Principal

 case class WebIDPrincipal(webid: java.net.URI) extends Principal {
  val getName = webid.toString
 }

  Useful because the WebID Profile can contain more up to date info about the user. I have just implemented this type of verification in WebIDAuthN [2] which is designed to work for Play2.0.


  C. CA verification
  ------------------

  If one trusts the CA and the signatures match then anything said in the certificate can be trusted
to that extent. This is the default for most Java servers.

   So having distinguished those, we would like to enable more flexibility than all the
existing java platforms do, and do this securely. It is currently possible in Tomcat [3] and most
Java servers to disable the CA authentication verification. The Java Servlet can then still get
the Certificate through some horrible code like:

 (X509Certificate[]) request.getAttribute("javax.servlet.request.X509Certificate");

Apart from this not taking Futures/Promises into account, there is a big issue here: the code does not know on receiving the the X509Certificate what part of it has been verified. The coder will need to look at the
server configuration files to work this out. As a result dealing with certificates becomes a huge magical issue, steeped in mystery, and so of course close to unusable.

  Working with Monadic Claims
  ===========================

The answer to this is to make it clear to the program what it is that he can rely on, and what he could
if needed spend time verifying. One concept to help here is to distinguish what the program believes to be true, from what is claimed. This is in natural language the distinction between 

   "joe says that pigs fly and 2+2=4"
and
   "pigs fly"

You can assert the first without asserting the second. 

In my recent implementation of WebID I created a Claim Monad  [2]  defined like this using Scalaz
 
  trait Claim[+S] {
    protected val statements: S

    def verify[V](implicit fn: S=> V ): V
  }

The contained object statements is protected and can only be extracted via a verify method.
The full Monad methods are given by scalaz magic:

  object Claim {
    implicit val ClaimMonad: Monad[Claim] with Traverse[Claim] =
      new Monad[Claim] with Traverse[Claim] {

      def traverseImpl[G[_] : Applicative, A, B](fa: Claim[A])(f: A => G[B]): G[Claim[B]] =
        f(fa.statements).map(a => this.point(a))

      def point[A](a: => A) = new Claim[A]{ 
        protected val statements : A = a;
        def verify[V](implicit fn: A=> V ) = fn(statements)
      }

      def bind[A, B](fa: Claim[A])(f: (A) => Claim[B]) = f(fa.statements)
    }
  }

This allows one to have something like an X509 Claim and map it into a Claim[List[(URI, PublicKey)]]. Nothing has leaked outside of the claim, so the things inside may still be false in the possible world the program is running in/exploring.

A Claim is Traversable so that one transform a Claim[List[X]] into a List[Claim[X]] .

In everyday language: we can deduce from (It is claimed that pigs fly and 2+2=4) that (It is claimed that pigs fly) and (It is claimed that 2+2=4) 

Here then is part of the verification method:

   def verify(x509claim: Claim[X509Certificate]): 
            List[Promise[Validation[BananaException,WebIDPrincipal]]] = {
      val webidClaims: Claim[List[(String,PublicKey)]] = 
        for (x509 <- x509claim) yield {
         Option(x509.getSubjectAlternativeNames()).toList.flatMap { coll =>
          import scala.collection.JavaConverters.iterableAsScalaIterableConverter
          for {
            sanPair <- coll.asScala if (sanPair.get(0) == 6)
          } yield (sanPair.get(1).asInstanceOf[String].trim,x509.getPublicKey)
        }
      }
      val listOfClaims: List[Claim[(String,PublicKey)] =  webidClaims.sequence
      for ( webidclaim <- listOfClaims) yield verifyWebIDClaim(webidclaim)
  }

Each of the claims is verified returning a list of Validations Promises.
(validating each claim takes time - requiring perhaps an https request). 

As shown Claims are pretty simple to use, and make it easy to reason about what is not known and what
is verified.

  Going beyond Claims?
  ====================

What we need though is to know which parts of the claim have already been verified by the JVM. Moving away from CAs verification will make people nervous, and so we (may) want to allow the normal CA system to work for those that want it. But we also want it to be possible to be more flexible. Let us put aside all notions of data structure simplicity to start with, and just explore the data structures.

My current solution 

  trait RequestHeader { ... def certs: Promise[Seq[Certificate]] ... }

only works if we assume the CA authentication was enabled - or else it is not clear what the status of the Certificates are - are they verified or not?

If the web server never tried CA verification before passing the Certificate to the request, one could have

  trait RequestHeader { ... def certs: Promise[Claim[Seq[Certificate]]] ... }

this would not take into account the fact that the public key had been verified, but more importantly, what if it happens that we could have verified the Certificate using a CA? Then we loose the opportunity of authenticating someone - and probably someone quite serious, if they CA signed their cert. 

So we would perhaps like something like

  trait RequestHeader { ... def certs: Promise[VClaim[Certificate,Principal]]

where the VClaim is a type defined something like this

  type VClaim[C,V] = Pair[Claim[C],V]

or perhaps

  type VClaim[C,V] = Pair[Claim[C],List[Validation[Exception,V]]]

It could be wrapped so that one does not need to use the _1 and _2 methods to 
access each part of the VClaim. Something like this:

  trait VClaim[C,V] {
     def verified: List[Validation[Exception,V]]
     def claimed: Claim[C]
  }

  then code could be written like this

  header.certs.value.verified.map(principal => ... )


So we are looking for a data structure that can distinguish what is claimed from what is verified, only allow things to move out of claims via a verification method, and have something that can be composed and is simple to use. If one were not frightened of complexity one may even be interested in knowing how something was verified. For example knowning if the VClaim had done CA verification we could try WebID authentication.

  Perhaps this rings a bell for some one, and there is a well known way of doing this?

The above for example still leaves the question open as to whether we should not have

 trait RequestHeader { ... def certs: Promise[VClaim[Certificate,Certificate]]

  after all a CA verification would end up verifying the whole certificate, not just the Distinguished Names in the certificate....

  I think we are quite close to finding the right structure here. I would never have thought about Iteratees until I found them in Play2, so I thought perhaps some people with more experience in functional programming can point me to the right place.

	Henry

[1] available here with some very basic tests
     https://github.com/bblfish/play20 branch 2.0.3-with-TLS
   The next version of play will use scala 2.10 Futures, which should make things a lot more portable.
[2] https://github.com/read-write-web/rww-play/blob/0a9c5de5df73bbbcd468d4142f1cf5e05ba25ab3/app/org/w3/play/auth/WebIDAuthN.scala
[3] https://blogs.oracle.com/bblfish/entry/how_to_setup_tomcat_as


Social Web Architect
http://bblfish.net/

Received on Saturday, 11 August 2012 09:21:28 UTC