Re: [scalaz] partially validated claim data structure? Needed for TLS.
199 views
Skip to first unread message
Lars Hupel
Aug 12, 2012, 8:53:58 AM8/12/12
to sca...@googlegroups.com, Henry Story
Here are some thoughts from the top of my head:
If I understand the problem correctly, you'd like to have a data
structure holding multiple claims associated with potential verification
information, e.g. three claims, one of them unverified, one of them
where the verification failed, and one of them where it succeeded. Each
of these three "levels" might have a reason attached, e.g. "verification
failed" because of public key error, timeout, …
We can certainly "lift" some pieces of that into the `Claim[C]` type,
such that the *type* of the claim tells us what its level is.
Suppose the following:
trait Claim[L <: Level, S] {
private val statement: S
val level: L
// you might want a dedicated type for this verification functions
// apart from the simple `Function1`... because then your intent will
// become clear and you don't get any 'undesired' implicit values
def verify[M <: Level, V](implicit fn: Verificator[L, S, M, V]):
Claim[M, V]
// ...
}
`Verificator[L, S, M, V]` now elevates a claim of type `S` from level
`L` to level `M` while producing a new statement of type `V`.
On the other hand, `Level` is an arbitrary type where you can create
subclasses to denote the levels to your liking.
The `Monad` instance would be parametrized on `L`:
implicit val ClaimMonad[L <: Level] =
new Monad[({ type λ[α] = Claim[L, α] })#λ] {
def point[A](a: => A): Claim[L, A] = ???
def bind[A, B](fa: Claim[L, A])(f: A => Claim[L, B]): Claim[L, B] = ???
}
In your `RequestHeader`, you could store those claims:
trait RequestHeader {
type L <: Level
def certs: Promise[Claim[L, Seq[Certificate]]]
}
This way, you could be sure that all the claims in your header have a
certain minimum level (I guess `Claim` needs to be covariant in `L`,
too). Also, you would stay the whole time in your `Claim` structure
(which might be beneficial for future uses).
Now, to the conclusion. This approach adds some type information to your
`Claim` which makes it easier to "trust" an expression, because the
compiler checks whether the computations are sound (this resembles
information flow security/security type systems).
If that's not what you're after, another idea would be to just write
`VClaim` as
List[Either[Claim[C], Validation[Exception, V]]]
i.e. a list of elements which are either a (not-yet-verified) claim or
are invalid (`Exception`) or valid (`V`).
Hope that helps
Lars
If I understand the problem correctly, you'd like to have a data
structure holding multiple claims associated with potential verification
information, e.g. three claims, one of them unverified, one of them
where the verification failed, and one of them where it succeeded. Each
of these three "levels" might have a reason attached, e.g. "verification
failed" because of public key error, timeout, …
We can certainly "lift" some pieces of that into the `Claim[C]` type,
such that the *type* of the claim tells us what its level is.
Suppose the following:
trait Claim[L <: Level, S] {
private val statement: S
val level: L
// you might want a dedicated type for this verification functions
// apart from the simple `Function1`... because then your intent will
// become clear and you don't get any 'undesired' implicit values
def verify[M <: Level, V](implicit fn: Verificator[L, S, M, V]):
Claim[M, V]
// ...
}
`Verificator[L, S, M, V]` now elevates a claim of type `S` from level
`L` to level `M` while producing a new statement of type `V`.
On the other hand, `Level` is an arbitrary type where you can create
subclasses to denote the levels to your liking.
The `Monad` instance would be parametrized on `L`:
implicit val ClaimMonad[L <: Level] =
new Monad[({ type λ[α] = Claim[L, α] })#λ] {
def point[A](a: => A): Claim[L, A] = ???
def bind[A, B](fa: Claim[L, A])(f: A => Claim[L, B]): Claim[L, B] = ???
}
In your `RequestHeader`, you could store those claims:
trait RequestHeader {
type L <: Level
def certs: Promise[Claim[L, Seq[Certificate]]]
}
This way, you could be sure that all the claims in your header have a
certain minimum level (I guess `Claim` needs to be covariant in `L`,
too). Also, you would stay the whole time in your `Claim` structure
(which might be beneficial for future uses).
Now, to the conclusion. This approach adds some type information to your
`Claim` which makes it easier to "trust" an expression, because the
compiler checks whether the computations are sound (this resembles
information flow security/security type systems).
If that's not what you're after, another idea would be to just write
`VClaim` as
List[Either[Claim[C], Validation[Exception, V]]]
i.e. a list of elements which are either a (not-yet-verified) claim or
are invalid (`Exception`) or valid (`V`).
Hope that helps
Lars
Henry Story
Aug 15, 2012, 12:06:12 PM8/15/12
to sca...@googlegroups.com, Henry Story, hu...@in.tum.de
Hi Lars,
thanks for those ideas. They seem like they do address the question
I had. I will need to implement it, to get see if they fit. That will be in
a little over a week, as I am off to a philosophy conference...
In the meantime I have some authentication working already in the
rww-play project using the simple Future[Seq[Certificate]] method
Thanks again for you those ideas. I'll get back to this thread,
in 10 days or so.
Henry
Henry Story
Sep 18, 2012, 9:46:28 AM9/18/12
to sca...@googlegroups.com, play-fr...@googlegroups.com, Lars Hupel
This is the continuation of a question I asked last month on the Play and scalaz mailing lists [1], cerning how to change the RequestHeader interface to allow the fetching of client certificates, something the WebID protocol ( http://webid.info/ is going to make a lot more useful to do )
Currently I added patched Play 2.0.3 [2] for it to have the following signature
trait RequestHeader {
def certs: Promise[Seq[Certificate]] ...
}
This, as I mentioned previously, is a huge improvement over what java frameworks provide [3] mostly because it deals in Futures (aka Promises), allowing for asynchronous operations.
What is missing is that the certificates need to be wrapped in some object that tells us how the Certificates were verified. Since there are a number of ways they can be verified (eg: using the traditional CA verification procedure, or the more flexible http://webid.info/ one ) we could genericise on that field like this:
trait RequestHeader[M[_]] { //...
type Certificates = Seq[Certificate]
def certs: Promise[M[Certificates]]
}
One could then have a number of implementations of RequestHeader[M[_]].
1) one simple one for servers that functioned the standard Java way, by verifying the signature of the Certificate Authority on the certificate chains using the Trust Store. The signature would then be
trait RequestHeaderTraditional extends RequestHeader[Id] {
def certs: Promise[Id[Certificates]]
}
which for coders is the same as
trait RequestHeaderTraditional extends RequestHeader[Id] {
def certs: Promise[Certificates]
}
which is what the current Play 2.0 patch does. This would be quite standard and so not surprising devs unduly.
2) Then there could be another version that used a simple claim as I suggested in my previous mail
trait RequestHeaderMin extends RequestHeader[Claim] {
def certs: Promise[Claim[Certificates]]
}
The good thing about this is that "servlet" like code written for servers doing verification of type (1) would not be loaded if the server were started in mode (2). This would remove all kinds of security holes due to a misunderstanding by local code of the environmental security constraints. Ie: code assuming the certificate it received had been fully verified, when in fact it had not.
3) One could then extend this and have more evolved versions of Claims such as the one proposed by Lars Hupel below. These could try to keep track of how certificates were verified, the trust one has in CAs, and perhaps many other things. Further down the line, this could allow one to be very flexible by verifying Certificates the CA way, if possible, and if not to still pass a non verified certificate to the "servlet" code in such a way that it would not be mislead.
I am not yet sure how much work it would be to rewrite the RequestHeader trait in Play2.0 to be generic like that...So I wonder what the play2.0 folks think of this solution.
Henry
[1] https://groups.google.com/d/topic/scalaz/0v0mv_2-WDw/discussion
It has taken me a bit of time to respond because I spent a few weeks preparing for a philosophy conference, and then also spent a lot of time then studying scalaz thanks to many great articles that have been put together by http://eed3si9n.com/ in his "Learning Scalaz" series.
[2] available here with some very basic tests
https://github.com/bblfish/play20 on br1anch 2.0.3-with-TLS
The next version of play will use scala 2.10 Futures, which should make things a lot more portable. Also see the pull request here:
https://github.com/playframework/Play20/pull/340
[3] it is just a huge improvement over a call such as this:
req.getAttribute("javax.servlet.request.X509Certificate")
that has to be cast, don't have a notion of future, and is plain ugly
http://www.coderanch.com/t/438788/Security/Read-client-certificate-Servlet
Social Web Architect
http://bblfish.net/
Currently I added patched Play 2.0.3 [2] for it to have the following signature
trait RequestHeader {
def certs: Promise[Seq[Certificate]] ...
}
This, as I mentioned previously, is a huge improvement over what java frameworks provide [3] mostly because it deals in Futures (aka Promises), allowing for asynchronous operations.
What is missing is that the certificates need to be wrapped in some object that tells us how the Certificates were verified. Since there are a number of ways they can be verified (eg: using the traditional CA verification procedure, or the more flexible http://webid.info/ one ) we could genericise on that field like this:
trait RequestHeader[M[_]] { //...
type Certificates = Seq[Certificate]
def certs: Promise[M[Certificates]]
}
One could then have a number of implementations of RequestHeader[M[_]].
1) one simple one for servers that functioned the standard Java way, by verifying the signature of the Certificate Authority on the certificate chains using the Trust Store. The signature would then be
trait RequestHeaderTraditional extends RequestHeader[Id] {
def certs: Promise[Id[Certificates]]
}
which for coders is the same as
trait RequestHeaderTraditional extends RequestHeader[Id] {
def certs: Promise[Certificates]
}
which is what the current Play 2.0 patch does. This would be quite standard and so not surprising devs unduly.
2) Then there could be another version that used a simple claim as I suggested in my previous mail
trait RequestHeaderMin extends RequestHeader[Claim] {
def certs: Promise[Claim[Certificates]]
}
The good thing about this is that "servlet" like code written for servers doing verification of type (1) would not be loaded if the server were started in mode (2). This would remove all kinds of security holes due to a misunderstanding by local code of the environmental security constraints. Ie: code assuming the certificate it received had been fully verified, when in fact it had not.
3) One could then extend this and have more evolved versions of Claims such as the one proposed by Lars Hupel below. These could try to keep track of how certificates were verified, the trust one has in CAs, and perhaps many other things. Further down the line, this could allow one to be very flexible by verifying Certificates the CA way, if possible, and if not to still pass a non verified certificate to the "servlet" code in such a way that it would not be mislead.
I am not yet sure how much work it would be to rewrite the RequestHeader trait in Play2.0 to be generic like that...So I wonder what the play2.0 folks think of this solution.
Henry
[1] https://groups.google.com/d/topic/scalaz/0v0mv_2-WDw/discussion
It has taken me a bit of time to respond because I spent a few weeks preparing for a philosophy conference, and then also spent a lot of time then studying scalaz thanks to many great articles that have been put together by http://eed3si9n.com/ in his "Learning Scalaz" series.
[2] available here with some very basic tests
https://github.com/bblfish/play20 on br1anch 2.0.3-with-TLS
The next version of play will use scala 2.10 Futures, which should make things a lot more portable. Also see the pull request here:
https://github.com/playframework/Play20/pull/340
[3] it is just a huge improvement over a call such as this:
req.getAttribute("javax.servlet.request.X509Certificate")
that has to be cast, don't have a notion of future, and is plain ugly
http://www.coderanch.com/t/438788/Security/Read-client-certificate-Servlet
http://bblfish.net/
Henry Story
Sep 20, 2012, 9:13:13 AM9/20/12
to Lars Hupel, sca...@googlegroups.com
Hi Lars,
I have been exploring your suggestions below, and placed the code online
https://github.com/bblfish/scalaz-playground/blob/57d91b380f4bd9b468a35bb011edd81d80226211/src/main/scala/RequestHeader.scala
There I have simplified the problem to the minimum so that one does not get lost in complexities of HTTP or X509. There is a Web object that returns Documents, that have primary topics that have public keys. Public Keys are just BigIntegers.
So the code works as far as extracting statements from Monads that are True, as one can see in the code in the Test object (line 150). The problem I am having is that Monads don't allow one with map and flatMap to map an object to a different Monad. So a Claim[Level0,Cert] can be mapped to Claim[Level0,X] but the level cannot be changed, which is a bit what we need in the Verification
class in order to be able to map across Claim Levels.
There is some commented out code that line 118 that won't compile because of that.
I am pursuing this...
Henry
Ps. the suggestion of a very generic
trait RequestHeader[M[_]] {
def cert: Promise[M[Certificates]]
}
may require I think a lot of rewriting of Play. I wonder
if there is a way to reduce the rewriting. Perhaps by
using a type as in
trait RequestHEader {
type M[_]
def cert: Promise[M[Certificates]]
I have been exploring your suggestions below, and placed the code online
https://github.com/bblfish/scalaz-playground/blob/57d91b380f4bd9b468a35bb011edd81d80226211/src/main/scala/RequestHeader.scala
There I have simplified the problem to the minimum so that one does not get lost in complexities of HTTP or X509. There is a Web object that returns Documents, that have primary topics that have public keys. Public Keys are just BigIntegers.
So the code works as far as extracting statements from Monads that are True, as one can see in the code in the Test object (line 150). The problem I am having is that Monads don't allow one with map and flatMap to map an object to a different Monad. So a Claim[Level0,Cert] can be mapped to Claim[Level0,X] but the level cannot be changed, which is a bit what we need in the Verification
class in order to be able to map across Claim Levels.
There is some commented out code that line 118 that won't compile because of that.
I am pursuing this...
Henry
Ps. the suggestion of a very generic
trait RequestHeader[M[_]] {
def cert: Promise[M[Certificates]]
}
may require I think a lot of rewriting of Play. I wonder
if there is a way to reduce the rewriting. Perhaps by
using a type as in
trait RequestHEader {
type M[_]
def cert: Promise[M[Certificates]]
Henry Story
Sep 20, 2012, 5:07:49 PM9/20/12
to Lars Hupel, sca...@googlegroups.com
Ok, Got it to work, with a bit of thought.
https://github.com/bblfish/scalaz-playground/blob/master/src/main/scala/RequestHeader.scala
It was my Verificator.verify method that was problematic.
So now I can extract things that either are true (CA Signed) or that can be verified ( e.g., a WebID ). Indeed the verification can succeed or fail.
What would be interesting is if one could build up resulting pages inside unverified monads: So that I could build up a page to serve back to the user where I call him whatever he wants me to call him. I will act as if that was his real name - i.e. act as if that context were the actual world. (if we can think in terms of madal logic [1])
So currently for example I can't really prove that the CN in the certificate is his. But I don't really care, so long as I am just dealing with him, and not merging information from another context.
Any thoughts about that? My guess is that one could write a Web Server with this as the core concept...
Henry
[1] https://blogs.oracle.com/bblfish/entry/the_fifth_dimension
https://github.com/bblfish/scalaz-playground/blob/master/src/main/scala/RequestHeader.scala
It was my Verificator.verify method that was problematic.
So now I can extract things that either are true (CA Signed) or that can be verified ( e.g., a WebID ). Indeed the verification can succeed or fail.
What would be interesting is if one could build up resulting pages inside unverified monads: So that I could build up a page to serve back to the user where I call him whatever he wants me to call him. I will act as if that was his real name - i.e. act as if that context were the actual world. (if we can think in terms of madal logic [1])
So currently for example I can't really prove that the CN in the certificate is his. But I don't really care, so long as I am just dealing with him, and not merging information from another context.
Any thoughts about that? My guess is that one could write a Web Server with this as the core concept...
Henry
[1] https://blogs.oracle.com/bblfish/entry/the_fifth_dimension
Henry Story
Sep 30, 2012, 12:43:29 PM9/30/12
to Lars Hupel, sca...@googlegroups.com, Alexandre Bertails
Alexandre Bertails pointed out to me that this version won't work, because it is
using generics which work at compile time but not at execution time. The point of
setting this up is so that the admin can run the server in CA verified mode, or
non CA verified mode, so this is a runtime setting...
I am going to go back to the simpler method I thought of initially.
Henry
using generics which work at compile time but not at execution time. The point of
setting this up is so that the admin can run the server in CA verified mode, or
non CA verified mode, so this is a runtime setting...
I am going to go back to the simpler method I thought of initially.
Henry
Henry Story
Sep 30, 2012, 1:04:42 PM9/30/12
to play-fr...@googlegroups.com, sca...@googlegroups.com, Alexandre Bertails
I have implemented a test version of a simplified Play2.0 RequestHeader that can fetch a client
certificate asynchronously. You need asynchronicity, because making the request may require
the user to select his certificate in the browser...
This version is very simple - it does not require one to run Play2.0 or patch it -
purely in order to explore what the best data structure for the RequestHeader would
be.
The current code has a clear but very verbose type. But it should be a good starting
point to develop more user friendly ( Play2.0 compliant ) data structure. The code is on
github [1] and it uses scalaz which avoids all kinds of monad and other boilerplate.
It simplifies the web and certificate based mechanisms down to the minimum of what
we really need so that we don't get lost in the ASN.1 rat hole whilst trying to build
a nice data structure.
I simplify certificated down to this - BigInts standing for public keys
case class Cert(cn: String, pubKey: BigInt, subjectAltNames: List[URI] )
I can then define a RequestHeader
trait RequestHeader {
type Certs = Array[Cert] //in java cert chains are sent around in an Array
/**
* We return a Future that is either a Certificate verified by a CA (right)
* or a claim of a Certificate ( when it has not been verified by a CA )
* The Claim is useful if one wants to for example
* 1. create a service that shows the user the certificate received
* 2. use the public key as an identifier ( no need for a CA )
* 3. use the cert for WebID ( http://webid.info/ ) authentication
* @return Future of an Either ( \/ in scalaz )
*/
def cert: Future[\/[Claim[Certs],Certs]]
...
}
And a claim is again the monadic ( using scalaz to remove the Monad boilerplate )
trait Claim[+S] {
protected val statements: S
def verify[V](implicit fn: S=> V ): V
}
So this seems to work. But presumably for Play one should transform the return
type of the cert method from
Future[\/[Claim[Certs],Certs]]
to something simpler. Does anybody have some good ideas on how I go about that?
In a way of course that is functionally correct - that is why I am asking.
The code on github shows what the above datastructure permits one to do.
Henry
[1] https://github.com/bblfish/scalaz-playground/blob/c3b6e77b201619d9834c2bb8b192f46881d60f4e/src/main/scala/play/DynamicServer.scala
On 11 Aug 2012, at 16:00, Henry Story <henry...@gmail.com> wrote:
> I am looking for a way to improve on the usual implementation of TLS client certificate selection in a web server so as to go beyond what is offered in any Java Web framework, and have something a lot more efficient, more flexible, and that could help us perhaps finally make security something everyone can work with a lot more easily. Here I am thinking from work I have been developing in Play2.0 framework, but it should work just as well in any other framework. I am asking about this on the scalaz mailing list because I think that this is the most likely place where people would be able to point me to the best data structure to use. This should become clear in the explanation below.
>
> 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
> [3] https://blogs.oracle.com/bblfish/entry/how_to_setup_tomcat_as
> --
> You received this message because you are subscribed to the Google Groups "play-framework" group.
> To view this discussion on the web visit https://groups.google.com/d/msg/play-framework/-/4HymV88XWJoJ.
> To post to this group, send email to play-fr...@googlegroups.com.
> To unsubscribe from this group, send email to play-framewor...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/play-framework?hl=en.
certificate asynchronously. You need asynchronicity, because making the request may require
the user to select his certificate in the browser...
This version is very simple - it does not require one to run Play2.0 or patch it -
purely in order to explore what the best data structure for the RequestHeader would
be.
The current code has a clear but very verbose type. But it should be a good starting
point to develop more user friendly ( Play2.0 compliant ) data structure. The code is on
github [1] and it uses scalaz which avoids all kinds of monad and other boilerplate.
It simplifies the web and certificate based mechanisms down to the minimum of what
we really need so that we don't get lost in the ASN.1 rat hole whilst trying to build
a nice data structure.
I simplify certificated down to this - BigInts standing for public keys
case class Cert(cn: String, pubKey: BigInt, subjectAltNames: List[URI] )
I can then define a RequestHeader
trait RequestHeader {
type Certs = Array[Cert] //in java cert chains are sent around in an Array
/**
* We return a Future that is either a Certificate verified by a CA (right)
* or a claim of a Certificate ( when it has not been verified by a CA )
* The Claim is useful if one wants to for example
* 1. create a service that shows the user the certificate received
* 2. use the public key as an identifier ( no need for a CA )
* 3. use the cert for WebID ( http://webid.info/ ) authentication
* @return Future of an Either ( \/ in scalaz )
*/
def cert: Future[\/[Claim[Certs],Certs]]
...
}
And a claim is again the monadic ( using scalaz to remove the Monad boilerplate )
trait Claim[+S] {
protected val statements: S
def verify[V](implicit fn: S=> V ): V
}
So this seems to work. But presumably for Play one should transform the return
type of the cert method from
Future[\/[Claim[Certs],Certs]]
to something simpler. Does anybody have some good ideas on how I go about that?
In a way of course that is functionally correct - that is why I am asking.
The code on github shows what the above datastructure permits one to do.
Henry
[1] https://github.com/bblfish/scalaz-playground/blob/c3b6e77b201619d9834c2bb8b192f46881d60f4e/src/main/scala/play/DynamicServer.scala
On 11 Aug 2012, at 16:00, Henry Story <henry...@gmail.com> wrote:
> I am looking for a way to improve on the usual implementation of TLS client certificate selection in a web server so as to go beyond what is offered in any Java Web framework, and have something a lot more efficient, more flexible, and that could help us perhaps finally make security something everyone can work with a lot more easily. Here I am thinking from work I have been developing in Play2.0 framework, but it should work just as well in any other framework. I am asking about this on the scalaz mailing list because I think that this is the most likely place where people would be able to point me to the best data structure to use. This should become clear in the explanation below.
>
> 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
> --
> You received this message because you are subscribed to the Google Groups "play-framework" group.
> To view this discussion on the web visit https://groups.google.com/d/msg/play-framework/-/4HymV88XWJoJ.
> To post to this group, send email to play-fr...@googlegroups.com.
> To unsubscribe from this group, send email to play-framewor...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/play-framework?hl=en.
Reply all
Reply to author
Forward
0 new messages