Type-driven configuration management with Propellor

One often hears the "infrastructure as code" refrain when configuration-management systems are discussed. Normally, though, that phrase doesn't bring into mind an image of infrastructure as Haskell code. In his 2017 linux.conf.au talk, Joey Hess described his Propellor system and the interesting features that a Haskell implementation makes possible, with a special focus on how Haskell's type-checking system can be pressed into service to detect configuration errors.

What are, Hess asked, the best practices for configuration management these days? Configuration files should have a simple format, to begin with. A declarative approach is better than an imperative approach; one of the good things that systemd brought to the table was declarative configuration. It should be compositional, since we tend to configure systems by composing various components together. He suggested that these points should be kept in mind during the talk.

Take two well-known systems for comparison: Ansible and Puppet. They both use a simple file format, though he put "simple" in quotes when describing Ansible. This format is extended, in either case, with features like variables. Ansible adds conditionals and loops, while Puppet uses a separate language for control structures. The Ansible configuration file format is Turing-complete, while the Puppet language may not be.

In general, Turing-complete configuration files are not seen as being a good idea. That leads to the classic Turing tarpit situation where everything is possible but nothing of interest is easy. The sendmail.cf format and others have taught us that we don't want Turing-complete configuration languages; if you can write the Towers of Hanoi in your configuration language, he said, you're doing something wrong. A Turing-complete language is also not declarative, violating another one of the best practices listed above.

That said, there are some advantages that can come from a Turing-complete language. You can create embedded, domain-specific languages that make common tasks easy. And, central to this talk, you can use the language's type-checking system to help avoid the creation of bad configurations.

Introducing Propellor

Propellor is a system that he wrote, similar to Ansible or Puppet. It goes out to hosts and does things to them to make those hosts look the way they are supposed to be. But it's all done in Haskell. To drive that point home, Hess jumped right in by putting up a slide containing this code:

    main :: IO ()
    main = defaultMain hosts

    hosts :: [Host]
    hosts = [foo, bar]

    foo :: Host
    foo = host "foo.example.com" $ props
        & osDebian (Stable "jessie") X86_64
	& Apt.stdSourcesList
	& Apt.installed ["openssh-server"]

That is, he acknowledged, a lot of code, "but don't worry, there will be lots more later". The first two lines just indicate that this is a main program and can be ignored. The next two indicate that there are two hosts to be managed, foo and bar. The last group describes the host foo in more detail, giving its host name and a number of properties. It's an X86_64 server running Debian jessie, with the standard list of package sources set up and the OpenSSH server installed. In the above example, the double-colon (::) is a declaration with a type. So hosts is a list of Host, while foo is a singleton Host.

Properties are the basic building block of the configuration system; they are something you can say about a system. There are a number of other data types built into Propellor to describe host architectures, packages, users, groups, port numbers, and around 150 other attributes. Using so many types brings a number of advantages, starting with the fact that the compiler can catch and flag typos.

The real reason for using types, though, is that Haskell types let you prove things about programs. In this setting, it lets you prove things about configured systems and avoid a lot of problems.

Composition and types

Systems are built through the composition of multiple components and configurations, so system descriptions consist of composed properties. Properties can be composed in four different ways, each of which is expressed as a function that takes two properties and returns yet another property. The composition functions in Propellor are requires, before, fallback, and onChange. He showed the definition of a securefoo property that looked like:

    securefoo :: Property
    securefoo =
        Apt.installed ["foo"]
	   `requires` File.containsLines "/etc/foo" ["secure=1"]
	   `onChange` Service.restarted "foo"

Here, the Apt.installed property ensures that the foo package is installed. It is then composed, using the infix requires function, with a property requiring that the secure=1 line appears in /etc/foo. That is then composed with another property causing foo to be restarted when a change is made.

This kind of composition is powerful, he said, but all compositions are the same; there's nothing here yet that is helping to prevent problems. It would be nice to do better, and make bad combinations of properties be a type error. To that end, he started adding types, the first of which was RevertableProperty, indicating a property that can be reverted. The installation of a package is revertable, while the architecture of the system is not, for example. Consider the following:

    bar :: RevertableProperty
    bar = Apt.installed ["bar"] <!> Apt.removed ["bar"]

This defines bar as a revertable property. Normally, it directs that the bar package should be installed:

    foo :: Host
    foo = Host "foo.example.com $ props
        & osDebian (stable "jessie") X86_64
	& Apt.stdSourcesList
	& bar

If, however, the desire is to ensure that the bar package is absent from the system known as foo, one could write instead:

    foo :: Host
    foo = Host "foo.example.com $ props
        & osDebian (stable "jessie") X86_64
	& Apt.stdSourcesList
	! bar

That will cause bar to be removed from the target system, should it be present. It would be a mistake, though, to try to revert the osDebian property:

    foo :: Host
    foo = Host "foo.example.com $ props
        ! osDebian (stable "jessie") X86_64
	& Apt.stdSourcesList
	! bar

The above code would cause the compiler to complain since that property is not revertable. Composition can also be type-checked in this way; if a revertable property is created with a requires composition, and one of the component properties is not revertable, a type error will result. This mechanism isn't perfect, he said, but it's good enough to model the system without trying to pin down every detail.

Containers

Propellor supports four different container types: Docker, systemd, chroot, and FreeBSD jails; it can create images for any of those types. Creating a container would be done with language like this:

    webserver :: Systemd.container
    webserver = systemd.debContainer "webserver" $ props
        & osDebian Testing X86_64
	& Apt.installedRunning "apache2"
	& Systemd.bind "/var/www"

Here, webserver is defined as being a systemd container and given various properties consistent with running a web server. Systemd.container is, in essence, another way of composing properties describing a desired container. This container could then be built and deployed on host foo with:

    foo :: Host
    foo = host "foo.example.com $ props
        & Systemd.nspawned webserver

"Just like that" you have a web-serving container running on foo. If the configuration file is later edited, Propellor will reach inside this container and make any needed changes; it doesn't need to rebuild the container from scratch.

More types

An early addition to Propellor was domain name system (DNS) configuration. The natural thing to do was to make an IP address be a property; each host has its IP address attached to it as one of its many properties. The configuration for the DNS server can then just look through the list of hosts using type introspection, find all the IP-address properties, and construct the DNS zone file accordingly. This works by adding an Info type to properties that need to provide information about a host.

That leads to a composition problem when containers are being used. Properties can add Info to both hosts and containers. When the two are composed, the Info must be propagated accordingly. Making that work required splitting the Property type into two variants, one that carries Info and one that does not. That was "the gateway drug" that led to further refinements of the Property type.

Once FreeBSD support was added, it became clear that some refinements were indeed needed. One wouldn't want to compose Debian-specific properties into a FreeBSD system, after all. So he added a "DebianLike" property type, along with "FreeBSD", "UnixLike", and more. Even more complexity can happen; for example:

    Property (HasInfo + DebianLike)

describes a property that carries Info and is applicable to Debian systems. The plus sign above indicates the addition of types — which is the sort of thing that Haskell developers apparently like to do. With this structure in place, the type checker can catch a new class of errors, such as using a FreeBSD-specific property on a Debian host.

Of course, it is nicer to make things just work than it is to flag errors. The system as described so far can catch an attempt to use the wrong package manager for a given host, but cannot yet express concepts like "just install this package" in a host-independent way. That sort of abstraction can be created with code like:

    Apt.upgraded :: Property DebianLike
    Pkg.upgraded :: Property FreeBSD

    upgraded :: Property (Debianlike + FreeBSD)
    upgraded = Apt.upgraded `pickOS` Pkg.upgraded

The result is a property (upgraded) that is both DebianLike and FreeBSD. The use of the pickOS composition function here allows that property to ensure that a package is current regardless of the target operating system.

Ongoing work

For a final example, involving code that isn't yet in the stable Propellor release, Hess delved into the detection of port-number conflicts. He often runs Tor bridges on his hosts, if he has the bandwidth available and port 443 (HTTPS) is not being used. If he later decides he needs a web server running on one of those hosts, he could end up with a runtime conflict over that port. Avoiding such conflicts is part of why Propellor exists in the first place, so some sort of solution is needed.

That solution looks like this:

    webserver :: Property (UsingPort 80 + UsingPort 443 + DebianLike)
    torBridge :: Property (UsingPort 443 + DebianLike)

A bit of programming at the Haskell type level ensures that an attempt to combine two properties using the same port will fail (while combining two DebianLike properties is fine). It works, but it has led to a situation where the type and the configuration need to be kept in sync. It could maybe be fixed by automatically generating the web-server configuration from the type information, but he hasn't gotten that far. There could also be problems with virtual hosts; that seems like it could get "really hairy" and he hasn't gotten there yet.

He concluded by putting up a pie chart displaying the number of errors avoided by each the techniques described above — before admitting that it was all made up. But the type checking has helped him to avoid a lot of mistakes; it is "a big win". (Readers wanting all the details, including a fair amount of discussion and bonus material in the question-and-answer period, may want to watch the video of the talk).

[Your editor would like to thank linux.conf.au and the Linux Foundation for assisting with his travel to the event.]

Index entries for this article
Conference	linux.conf.au/2017

---

to post comments