About That Type Theory

 NO  Comments Off on About That Type Theory
Jan 252013
 

I got the new bugzilla to work (kind of time consuming, but surprisingly straightforward), and … I guess it’s a bit of an improvement. In the process of converting the htaccess files of bugzilla into domtool config, I discovered that you can’t put filesMatch inside of directory thanks to some fancy context nesting (directory and location both establish context Location; <FilesMatch> is only valid in a <Directory> so you lose…).

I … kind of stabbed at things aimlessly until it worked and then did it again and came up with adding a Directory context and allowing filesMatch inside of that. This means we’d need a new filesMatchAll or something to do what the current version does (sensible, since <FilesMatch> under a virtual host matches all sub-directories i.e. different behavior, different action … luckily, zero HCoop members are using filesMatch).

context Location;
+context Directory;

extern type location;
{{A valid URI prefix}}

extern val location : location -> ^Vhost & Location => [Vhost & !Location];
-extern val directory : your_path -> ^Vhost & Location => [Vhost & !Location];
+extern val directory : your_path -> ^Vhost & Directory & Location => [Vhost & !Directory & !Location];
{{Set some configuration specific to a URI prefix or filesystem directory,
respectively.}}

extern type regexp;
{{PCRE regular expression}}

-extern val filesMatch : regexp -> ^Vhost & Location => [Vhost & !Location];
+extern val filesMatch : regexp -> ^Vhost & Location => [^Vhost & Directory & Location];
{{Mark nested configuration to only apply to filenames matching the regexp.}}

Problem: my reading of the language reference implies that there is only one context on top of the stack at a time, and there is no sequencing operator for matching a chunko of the stack. So my Directory & Location type might only check because of an accidental property of the type checker. Relying on accidents for things is clearly a bad idea…

I’m pretty sure being able to push more than one context onto the stack at once is a desirable property, so I have to wonder if this intentionally works.

I spent a couple of hours digging around in the type checker code and yow! It seems like it ought to be sensible, but it’s doing unfamliar things in familiar ways so I guess it’s time to get out the ol’ pencil and paper and trace through the checking process for an expression I know is correct to get a feel for how it all works. Or: plead for Adam to page this bit of knowledge back in and tell me if I’m an idiot or not if I agree to worship static type systems.

The last couple of months have been strange; I look back on the last three and a half years of hcoop and think I didn’t do enough, and then I realize that I only recently had the watershed moment where slamming my head against UNIX enough times led to me knowing what I’m doing. The worst part is nothing is too complicated, but the breadth of knowledge required is astounding.

Except for domtool, which requires that I learn how to exercise discipline with types instead of living in the delightfully inconsistent freewheeling Land of Lisp.

Domtool SSL vhosts… Oh the Joy

 NO  Comments Off on Domtool SSL vhosts… Oh the Joy
Jan 222013
 

Once upon a time, basically no one used SSL at HCoop, because you needed a dedicated IP and it was generally a pain. So we never really got any decent documentation (it manages to just not explain things like what kind of certificate we need). And it seems that the way SSL is implemented in Domtool is kind of a hack. Now that TLS SNI works out of the box, I suspect members might want to actually use SSL.

To create an SSL vhost today:


dom "foo.bar" with
  web "baz" where
    SSL = use_cert "/etc/apache2/ssl/user/myfancycert.pem";
  with
    serverAliasDefault;
  end;
end;

Setting the SSL environment variable causes Domtool to turn on the SSLEngine, change the ports, etc. This works for the simple case of a self-signed cert or one signed by a root certificate commonly distributed. Unfortunately, at least Gandi uses intermediate certificates that aren’t universally distributed to sign certificates (sensible), but those are signed by well known trusted root certificates. So: SSLCertificateChainFile must be supported.

Adding a new cacert permission and the trivial types and action needed to support it is easy, but there’s a problem: you can’t use the directive with the SSL engine off, and there’s no way to use the type checker to enforce this. My immediate workaround is just ignoring the directive during the eval phase when we’re not in an SSL vhost, but this isn’t clean. Of course, the kerberos authentication type also behaves this way, and the Domtool type system only promises to avoid creating maliciously invalid configuration.

It seems like contexts were designed just for this, and so the logical thing to do seems to be creating a new sslHost container of some sort that either goes inside or outside of vhost. Then, that container would declare an SSL context and the typing for any ssl dependent commands would do the right thing. But: which way is best? I’m not a type theorist, making this probably easy problem frustrating. Outside:

sslHosts with
    web "baz" where
      SSL = use_cert "/etc/apache2/ssl/user/myfancycert.pem";
    with
      serverAliasDefault;
    end;
  end;

My first thoughts were that this was the best way, but the only advantage seems being able to define a number of SSL vhosts at once (but we have abstraction in Domtool, negating that benefit). The disadvantages include continuing to allow users to shoot themselves in the foot by doing things like defining the SSL and non-SSL vhost for the same domain on different machines (probably a sign that the current and this approach are both Wrong™).

So, then, inside:


dom "foo.bar" with
  web "baz" where
    DocumentRoot = home "whatever";
  with
    serverAliasDefault;
    sslHost where
      SSL = use_cert "foo.pem";
    with
      serverAliasDefault;
    end;
  end;
end;

I think this is the Right Way ™ now. It prevents users from accidentally creating unreachable hosts and mandates that the SSL host configuration be kept with the other vhost configuration. At first glance, it might look hard to use (you’d have to duplicate the non-ssl and ssl vhost actions in both to make them identical), but yet again abstraction comes to the rescue and it would be trivial to define a function to duplicate the vhost body. Much of the time, the non-ssl host only exists to redirect to the ssl host as well, so this version would save some typing (at the keyboard) in the case.

The only thing that strikes me as possibly wrong is that the ssl vhost is under the vhost, when ssl-ness is more of an attribute of the vhost. Maybe the hierarchy doesn’t matter… I just fear that I would be abusing the context/predicate system. Perhaps instead there should be vhostSSL types (with easy domain webSSL/webSSLAt abstractions). This is what happens when a Lisp hacker inherits code from a type theory wizard.

Another possibility: actions can require that environment variables have certain types when they are invoked, and domtool uses predicates on base types to determine a refined type. Vhosts require that SSL be of type ssl which includes the value no_ssl; if you could refine an already refined type (you can’t, and there’s probably a good reason), a sane strategy might be to do that instead on any actions dependent upon SSL being enabled. Of course, that still doesn’t solve the problem of allowing users to create unreachable vhosts if they accidentally define the ssl and non-ssl vhosts on different nodes. Perhaps that has a different solution, or isn’t worth solving.