These are the slides from my vBSDcon talk on GELI work.
About a month ago, I started a discussion on freebsd-hackers and freebsd-security about a system for signed executables, with a focus on signed kernels and kernel modules. This is part of a larger agenda of mine to equip FreeBSD with OS-level tamper resistance features.
While the initial use of this is for signing the kernel and its modules, and checking signatures during the loader process as well as at runtime when kernel modules are loaded. However, it is desirable to build a system that is capable of growing in likely directions, such as executable and library signing.
This article details the current state of the design of this system.
I originally outlined a number of goals for this system:
- Be able to check for a correct cryptographic signature for any kernel or modules loaded at boot time for some platforms (EFI at a minimum)
- Be able to check for a correct cryptographic signature for any kernel module loaded during normal operations (whether or not to do this could be controlled by a sysctl, securelevel, or some similar mechanism)
- Work with what’s in the base system already and minimize new additions (ideally, just a small utility to sign executables)
- Minimize administrative overhead and ideally, require no changes at all to maintain signed kernel/modules
- Have a clear path for supporting signed executables/libraries.
- The design must support the case where a system builds locally and uses its own key(s) for signing kernels and modules (and anything else) and must allow the administrator complete control over which key(s) are valid for a given system (ie. no “master keys” controlled by central organizations)
- The design must allow for the adoption of new ciphers (there is an inevitable shift to post-quantum ciphers coming in the near future)
I also specified a number of non-goals:
- Hardware/firmware-based attacks are considered out-of-scope (there is no viable method for defending against them at the OS level)
- Boot platforms that don’t provide their own signature-checking framework up to loader/kernel can’t be properly secured, and are considered out-of-scope
- Boot platforms that impose size restrictions prohibiting incorporation of RSA and ED25519 crypto code (ex. i386 BIOS) are considered out-of-scope
- GRUB support is desirable, however it is not necessary to support GRUB out-of-the-box (meaning a design requiring reasonable modifications to GRUB is acceptable
There are several considerations that should weigh in on the design.
FreeBSD Base System
Unlike linux, FreeBSD has a base operating system which contains a number of tools and libraries which provide a set of operating system utilities. Most notably, the base system contains the OpenSSL (or in some cases, LibreSSL) crypto suite. This includes an encryption library as well as tools capable of creating and managing key-pairs and other cryptographic data in a variety of formats.
Additionally, the FreeBSD base system contains libelf, which is a library that provides mechanisms for manipulating ELF binaries. Additionally, the base system provides the binutils suite, including objcopy, which are command-line tools capable of manipulating ELF binaries.
Note that only some of these components (namely the signelf tool) exist at the present; the rest of the components exist only as man pages that describe them at present.
The FreeBSD kernel does not currently incorporate code for public-key cryptography, and direct incorporation of OpenSSL into the kernel has proven infeasible. Additionally, parsing code needs to be incorporated into the kernel for any formats that are used. Options here include incorporation of code from the NaCl library, which provides a very lightweight implementation of both RSA 4096 and Ed25519, as well as creating a minimal library out of code harvested from OpenSSL or LibreSSL.
A note on elliptic curve cryptography: the state of support for safe elliptic curves is sad. In my drafts of the man pages, I have mandated that the only acceptable curves are those that satisfy the security properties described by the SafeCurves project. At this time, these include M-221, E-222, Curve1174, Curve25519, E-382, M-383, Curve383187, Curve41417, Goldilocks-448, M-511, and E-521. Unfortunately, none of these is supported by OpenSSL at this time, though Curve25519 support is supposedly coming soon. However, I would prefer to write specs that mandate the right curves (and thus put pressure on crypto libraries) than cave to using bad ones.
Modifications to GRUB
GRUB provides the best option for FreeBSD coreboot support at this time. It also provides an existing mechanism for signing binaries. However, this mechanism is deficient in two ways. First, it relies on external signatures, which would complicate administration and require modification of virtually all installer programs, as well as run the risk of stale signatures. Second, it relies on the gnupg toolset, which is not part of the FreeBSD base system. Thus, it is inevitable that GRUB will need to be patched to support the signed executables proposed by this design. However, we should make efforts to keep the necessary changes as minimal as possible.
Signing and Trust System Design
The signing and trust system consists of a number of components, some of which are standards, some of which are interfaces, and some of which are tools. The core feature, of course, is the signed ELF convention. The signelf tool provides a one-stop tool for signing large numbers of executables. The trust system provides a system-level mechanism for registering and maintaining verification keys that are used to check signatures on kernel modules. Finally, the portable verification library provides a self-contained code package that can be dropped into the kernel, the loader, or a third-party codebase like GRUB.
Note that this design is not yet implemented, so it may be subject to change. Also, it has not yet undergone review on the FreeBSD lists, so it should be considered more of a proposal.
Signed ELF Binaries
The ELF format is very flexible, and provides a generic mechanism for storing metadata. The signed ELF convention utilizes this to store signatures in a special section within the binary itself. A signed ELF binary contains a section named .sign, which contains a detached PKCS#7 signature in DER encoding for the file. This signature is computed (and checked) on the entire file, with the .sign section itself being replaced by zero data of equal size and position.
Signing an ELF binary is somewhat involved, as it requires determining the size of a signature, creating a new section (along with its name), recomputing the ELF layout, computing the signature, and writing it into the section. Checking a signature is considerably simpler: it involves merely copying the signature, overwriting the .sign section with zeros, and then checking the signature against the entire file.
The PKCS#7 format was chosen because it is an established standard which supports detached signatures as well as many other kinds of data. The signatures generated for signed ELF files are minimal and do not contain certificates, attributes, or other data (a signature for RSA-4096 is under 800 bytes); however, the format is extensible enough to embed other data, allowing for future extensions.
The signelf Tool
Signed ELF binaries can be created and checked by adroit usage of the objcopy and openssl command-line tools. This is quite tedious, however. Moreover, there are certain use cases that are desirable, like signing a batch of executables using an ephemeral key, discarding the key, and generating a certificate for verification. The signelf tool is designed to be a simplified mechanism for signing batches of executables which provides this additional functionality. It is a fairly straightforward use of libelf and OpenSSL, and should be able to handle the binaries produced by normal compilation. Additionally, the signelf tool can verify signed ELF files. The signelf code is currently complete, and works on a kernel as well as modules.
The Trust System
In order to check signatures on kernel modules (and anything else), it is necessary to establish and maintain a set of trusted verification keys in the kernel (as well as in the boot loader). In order for this system to be truly secure, at least one trust root key must be built into the kernel and/or the boot loader, which can then be used to verify other keys. The trust system refers to the combination of kernel interfaces, standard file locations, and conventions that manage this.
System Trust Keys and Signing Keys
The (public) verification keys used to check signatures as well as the (private) signing keys used to generate signatures are kept in the /etc/trust/ directory. Verification keys are stored in /etc/trust/certs, in the X509 certificate format, and private keys are stored in /etc/trust/keys in the private key format. Both are stored in the PEM encoding (as is standard with many OpenSSL applications).
There is no requirement as to the number, identity, or composition of verification or signing keys. Specifically, there is not and will never be any kind of mandate for any kind of verification key not controlled by the owner of the machine. The trust system is designed to be flexible enough to accommodate a wide variety of uses, from machines that only trust executables built locally, to ones that trust executables built on an in-house machine only, to those that trust executables built by a third party (such as the FreeBSD foundation), or any combination thereof.
The preferred convention, however, is to maintain a single, per-machine keypair which is then used to sign any additional verification keys. This keypair should be generated locally for each machine, and never exported from the machine.
Trust Keys Library
Keys under /etc/trust/certs will be converted into C code constants and subsequently compiled into a static library providing the raw binary data for the keys during the buildworld process. This provides the mechanism for building keys into the kernel, loader, and other components. These keys are known as trust root keys, as they provide the root set for all trusted keys.
Kernel Trust Interface
The kernel trust interface provides access to the set of verification keys trusted by the kernel. This consists of an in-kernel interface as well as a user-facing device interface. The in-kernel interface looks like an ordinary key management system (KMS) interface. The device interface provides two primary mechanisms: access to the current set of trusted keys and the ability to register new keys or revoke existing ones.
Access to the existing database is accomplished through a read-only device node which simply outputs all of the existing trusted keys in PEM-encoded X509 format. This formatting allows many OpenSSL applications to use the device node itself as a CA root file. Updating the key database is accomplished by writing to a second device node. Writing an X509 certificate signed by one of the existing trusted keys to this device node will cause the key contained in the certificate to be added to the trusted key set. Writing a certificate revocation list (CRL) signed by a trusted key to the device node will revoke the keys in the revocation list as well as any keys whose signature chains depend on them. Trust root keys cannot be revoked, however.
This maintains the trusted key set in a state where any trusted key has a signature chain back to a trust root key.
Portable Verification Library
The final piece of the system is the portable verification library. This library should resemble a minimal OpenSSL-like API that performs parsing/encoding of the necessary formats (PKCS#7, X509, CRL), or a reduced subset thereof and public-key signature verification. I have not yet decided whether to create this from harvesting code from OpenSSL/LibreSSL or write it from scratch (with code from NaCl), but I’m leaning toward harvesting code from LibreSSL.
The trust system performs two significant roles in the system as planned, and can be expanded to do more things in the future. First, it ensures that loader only loads kernels and modules that are signed. Second, it can serve as a kind of system-wide keyring (hence the device node that looks like a typical PEM-encoded CAroot file for OpenSSL applications). The following is an overview of how it would operate in practice.
Signature Checking in the loader
In an EFI environment, boot1.efi and loader.efi have a chain of custody provided by the EFI secure boot framework. This is maintained from boot1.efi to loader.efi, because of the use of the EFI loaded image interface. The continuation of the chain of custody must be enforced directly by loader.efi. To accomplish this, loader will link against the trust key library at build time to establish root keys. These in turn can either be used to check the kernel and modules directly, or they can be used to check a per-kernel key (the second method is recommended; see below).
Per-Kernel Ephemeral Keys
The signelf utility was designed with the typical kernel build process in mind. The kernel and all of its modules reside in a single directory; it’s a simple enough thing to run signelf on all of them as the final build step. Additionally, signelf can generate an ephemeral key for signing and write out the verification certificate after it finishes.
This gives rise to a use pattern where every kernel is signed with an ephemeral key, and a verification certificate is written into the kernel directory. This certificate is in turn signed by the local trust root key (signelf does this as part of the ephemeral key procedure). In this case, the loader first attempts to load the verification certificate for a kernel, then it loads the kernel and all modules.
Signed Configuration Files
The FreeBSD loader relies on several files such as loader.4th, loader.conf, loader.menu, and others that control its behavior in significant ways. Additionally, one can foresee applications of this system that rely on non-ELF configuration files. For loader, the simplest solution is to store these files as non-detached PKCS#7 messages (meaning, the message and file contents are stored together). Thus, loader would look for loader.conf.pk7, loader.4th.pk7, and so on. A loader built for secure boot would look specifically for the .pk7 files, and would require signature verification in order to load them.
The keybuf Interface
The kernel keybuf interface was added in a patch I contributed in late March 2017. It is used by GELI boot support to pass keys from the boot phases to the kernel. However, it was designed to support up to 64 distinct 4096-bit keys without modification; thus it can be used with RSA-4096. An alternative to linking the trust key library directly into the kernel is to have it receive the trusted root key as a keybuf entry.
This approach has advantages and disadvantages. The advantage is it allows a generic kernel to be deployed to a large number of machines without rebuilding for each machine. Specifically, this would allow the FreeBSD foundation to publish a kernel which can make use of local trust root keys. The primary disadvantage is that the trust root keys are not part of the kernel and thus not guaranteed by the signature checking. The likely solution will be to support both possibilities as build options.
The preferred scheme for trust root keys is to have a local keypair generated on each machine, with the local verification certificate serving as the sole trust root key. Any vendor keys that might be used would be signed by this keypair and loaded as intermediate keys. Every kernel build would produce an ephemeral key which would be signed by the local keypair. Kernel builds originating from an organization would also be signed by an ephemeral key, whose certificate is signed by the organization’s keypair. For example, the FreeBSD foundation might maintain a signing key, which it uses to sign the ephemeral keys of all kernel builds it publishes. An internal IT organization might do the same.
It would be up to the owner of a machine whether or not to trust the vendor keys originating from a given organization. If the keys are trusted, then they are signed by the local keypair. However, it is always an option to forego all vendor keys and only trust locally-built kernels.
An alternate use might be to have no local signing key, and only use an organizational trust root key. This pattern is suitable for large IT organizations that produce lots of identical machines off of a standard image.
This design for the trust system and kernel/module signing is a comprehensive system-wide public-key trust management system for FreeBSD. Its initial purpose is managing a set of keys that are used to verify kernels and kernel modules. However, the system is designed to address the issues associated with trusted key management in a comprehensive and thorough way, and to leave the door open to many possible uses in the future.
I discovered the RISC-V project over the holidays, and promptly fell in love with it. RISC-V represents an expansion of the open-source ethos into the hardware space, and I believe it has the potential to be one of the most important open hardware projects in the long run.
Crypto is something I care about, and an open hardware project like RISC-V presents an excellent opportunity to introduce high-quality extensible hardware cryptographic functions. As I’m no stranger to computer architecture, I decided to roll up my sleeves and throw together a cryptographic instruction set extension for RISC-V.
This article is an overview of my design as it stands. I have a detailed draft specification and the beginnings of an implementation in a fork of Berkeley’s rocket-chip repository.
An on-chip crypto implementation affords a number of possibilities that can improve security. For one, hardware crypto implementations are able to control many kinds of side-channel attacks much more effectively than software. Hardware implementations can completely avoid timing, cache, and branch-predictor side-channels. In addition, my designs allow for fuzzing of physical side-channels through techniques such as pipelining and injection of random “dummy” operations.
In addition to side-channel mitigation, hardware crypto potentially allows for designs which specifically account for insecure memory and disk, keeping all unencrypted key material in the processor core and not allowing it to be exported as plaintext. This is a key principle in the design of hardware security modules (HSMs), and it would be a welcome feature in a general CPU.
Hardware Crypto Paradigms
There are roughly three dominant paradigms for hardware crypto. The first is a wholly-separate device connected via a system bus (such as PCI), which implements various functions. One of the key advantages of this is that the sensitive data can remain on the device, never accessible to the rest of the system (of course, this is also a disadvantage in the case of closed-source hardware, as we can never be certain that the system isn’t weakened or back-doored). However, this can’t rightly be considered an ISA extension, as it’s wholly-separate.
The other end of the spectrum is occupied by cipher-specific instructions such as Intel’s AESNI instruction set. These are often very efficient, as many cryptographic ciphers can be implemented very efficiently in hardware. However, they don’t do much for protection of sensitive data. Moreover, writing specific ciphers into the ISA is generally a bad idea: ciphers are sometimes broken, and more often phased out and replaced by newer, better algorithms. Moreover, such a practice can enshrine weak crypto, as is seen in the continuing use of weak and broken crypto like RC4, MD5, SHA1, DES, 3DES, and 1024-bit RSA in many hardware crypto offerings.
Coprocessors are a third possibility; however, a coprocessor still must design its own instruction set, and that design must still cope with the reality of changing cryptographic algorithms. Moreover, the interface between a general CPU and a coprocessor is complicated and difficult to design well.
I began by attempting to generalize the instruction-based approach, initially planning for special secure registers and a generalized framework for crypto instructions. This ended up evolving into a framework I call “engines” which is most similar to the device-based approach, except that it lives in the processor core and is directly integrated into the pipeline. The engines instruction set is also designed to allow the entire mechanism to be virtualized in an OS, and to allow for any engine to be implemented in software within a kernel.
An engine is essentially a larger, more complex functional unit which is capable of performing a single complex operation or a limited set of them. In a typical pipeline, an engine looks and feels essentially like a memory unit, and for most intents and purposes can be treated like one. After an engine has been configured, it is interacted with by means of a set of commands, which may supply arguments and may return results. These behave exactly like load and store instructions in that they may generate faults, and commands yielding results may stall until data is available.
Engines also exist in a number of states, and can be moved between states by a transition instruction. The uninitialized state represents an engine that is being configured (for example, a crypto engine needs to be supplied its key). Initialization may performing preprocessing on initialization data, and moves the engine into the ready state (for example, the AES cipher does precomputation of the key schedules). A ready engine can be started, causing it to enter the running state. This allows a distinction between engines that are simply prepared, and engines that may be executing random operations continuously to fuzz side-channels. To facilitate fast context-switching, a pause transition moves a running engine into the paused state, and ignores all other states, and the unpause transition restarts a paused engine. Lastly, engines can be transitioned into a saving state, where their state can be serialized, and an uninitialized engine can be placed in the resuming state, where a saved state can be reloaded.
Each core has a number of engine resources, which are referenced through engine handle registers. An acquire instruction attempts to acquire an engine resource of a particular type, storing it to an engine handle register. The namespace for engine resources is quite large, and can be further extended using CSRs to select a particular namespace. This allows the engines framework to function as a flexible mechanism for the indefinite future.
Engine Instruction Detail
The following is a description of each instructions the proposed engine ISA extension.
eng.acquire eh, code
The acquire instruction attempts to acquire an engine resource of type code, binding it to the engine handle eh if such a resource is available. If no such resource is available, it generates a fault trap (an OS can possibly use this along with the rebind instruction to implement engines in software).
The release instruction releases the engine resource bound to eh.
eng.ehsave eh, rd
The ehsave instruction saves the binding in eh to the ordinary register rd. For all hardware engine resources, this is guaranteed to be represented as a 32-bit number with the lowest bit clear. This convention allows an operating system to represent bindings to software implementations as numbers with the lowest bit set.
eng.rebind eh, rs
The rebind instruction re-establishes a binding to eh using the data in the in ordinary register rs. If the lowest bit is clear in rs, then the binding is checked against the actual hardware engine resources. Otherwise, it is taken to refer to a software implementation.
eng.trans eh, code
The trans instruction executes the state transition represented by code. It may generate a fault trap for bad transitions.
Saving and Restoring
eng.savecnt eh, rd
The savecnt instruction writes into rd the number of state words that needs to be saved in order to save the entire state of the engine handle eh. This can only be executed if the engine resource bound to eh is in the saving state.
eng.save eh, rd, rs
The save instruction writes the state word for the engine resource bound to eh at the index given in rs into the register rd. The highest valid index is equal to one less than the value given by the savecnt instruction. This can only be executed if the engine resource bound to eh is in the saving state.
eng.restore eh, rs1, rs2
The restore instruction writes the state word in rs2 to the index rs1 in the engine handle eh. The restore instruction must be executed for all indexes corresponding to a particular saved state in strictly ascending order. This instruction can only be executed if the engine resource bound to eh is in the restoring state.
The command instructions allow for varying numbers of arguments and results. All command instructions may stall for a finite amount of time, and may generate faults. Some command codes may be restricted to certain states.
eng.icmd eh, code
The icmd instruction executes the imperative command given by code on the engine resource bound to eh.
eng.rcmd eh, code, rd
The rcmd instruction executes the receive-only command given by code on the engine resource bound to eh. The result of the command is stored into rd.
eng.rs1cmd eh, code, rd, rs1
The rs1cmd instruction executes the send-receive command given by code on the engine resource bound to eh. The argument to the command is given in the rs1 register. The result of the command is stored into rd.
eng.rs2cmd eh, code, rd, rs1, rs2
The rs2cmd instruction executes the send-receive command given by code on the engine resource bound to eh. The arguments to the command are given in the rs1 and rs2 register. The result of the command is stored into rd.
eng.s1cmd eh, code, rs1
The s1cmd instruction executes the send-only command given by code on the engine resource bound to eh. The argument to the command is given in the rs1 register.
eng.s2cmd eh, code, rs1, rs2
The s2cmd instruction executes the send-only command given by code on the engine resource bound to eh. The arguments to the command are given in the rs1 and rs2 register.
eng.s3cmd eh, code, rs1, rs2, rs3
The s2cmd instruction executes the send-only command given by code on the engine resource bound to eh. The arguments to the command are given in the rs1 and rs2 register.
Example Crypto Engines
There are several sketches for example crypto engines, which show how this framework can be used for that purpose.
True Random Number Generator
A true random number generator using a physical process (such as electron or photon polarization, thermal noise, or other mechanisms) to generate random bits, which it accumulates in a ring-buffer. The generator is started with the start transition, and randomness can be read off with a receive-format command that blocks until enough randomness is available.
Symmetric Cipher Encryption/Decryption Pipeline
Symmetric cipher encryption and decryption demonstrates the side-channel fuzzing capabilities of hardware engines. The key material is loaded during the uninitialized state, and initialization does whatever preprocessing is necessary. When the engine is in the running state, it constantly generates “dummy” operations using pseudorandomly-generated keys, IVs, and data which are discarded from the pipeline upon completion. The implementation uses a pipeline to allow very high throughput of operations. Data is added to the pipeline with a two-argument send command, and read off with a receive command. Send and receive commands can generate deadlock faults if there is insufficient buffer space or data available.
Elliptic-Curve Point Multiplier
Elliptic curve point multiplication for a restricted set of elliptic curves can be implemented in a fashion similar to the symmetric cipher pipeline, except that for an elliptic curve multiplier, the pipeline typically cannot be completely unrolled. Finite field arithmetic modulo pseudo-mersenne primes can be implemented as a configurable circuit. Point multiplication can then be implemented using a ladder algorithm (such as the Montgomery ladder). The same random “dummy” operation injection suggested for symmetric ciphers can also be used here to fuzz side-channels.
Cryptographic hashes and message authentication codes transform an arbitrary amount of data into a fixed-size code. This is straightforward to implement in hardware, although the algorithms in question generally cannot be pipelined. In order to fuzz side-channels, we simply maintain some number of “dummy” internal states and keys in combination with the “real” one, and feed data to them at the same time as real data.
My original intent was to provide an extensible, general mechanism for supporting crypto on RISC-V hardware. The engines extension ended up becoming a much more general mechanism, however. In its most general form, this could even be considered an entire I/O instruction set. Regardless, the examples I have given clearly demonstrate that it can serve its original purpose very well.
The approach of applying pragmatics and principles of industrial programming language design to formal methods, verification, and dependently-typed languages is something I care a great deal about. It’s the focus of my programming language project Salt, and it was the subject of my recent lightning talk at IEEE SecDev and many of the discussions that followed.
Those who interact with me know I tend to talk about this subject quite a bit, and that I have a particular concern for the pragmatic aspects of language design. The origin of this concern no doubt comes from my time with the Java Platform Group at Oracle; there I saw the issues that a successful industrial language must confront firsthand and the demands that arise from real-world industrial use. I’ve also seen these sorts of issues in other places, like working on the FreeBSD and Linux kernels.
A common question I get is “what do you mean by ‘industrial language’?” I see this frequently in the context of the academic programming language and Haskell communities. I’ve seen this frequently enough that it’s prompted me to write an article on the topic.
Academic and Industrial PL
In my experience, there’s something of a gulf between academic knowledge about programming languages and industrial knowledge. Academic PL is primarily concerned with things like semantics, idealized language features, and type systems (particularly type systems). Academic PL knowledge is available through the usual academic conferences: POPL, PLDI, OOPSLA, ICFP, and the like, as well as various books and journals.
Industrial PL, by contrast, is generally less structured and accessible in its knowledge, existing primarily in the form of institutional knowledge in organizations like OpenJDK and others dedicated to maintaining major industrial languages. Some of this makes it out into industrial conferences (Brian Goetz, the Java language architect has given a number of talks on these subjects, such as this one).
In recent history, there has been a concerted effort by the industrial PL world to tap into this knowledge. This manifests in recent and upcoming Java language features as well as in languages like Rust which incorporate a number of advanced type system features. I saw this firsthand in my time on the Java Platform Group, and particularly in the work that went into the Lambda project and is now going into the Valhalla project.
Academic PL, on the other hand, has tended to be dismissive of the knowledge base of industrial PL as it lacks the kind of formalism that modern academic PL work demands. The source of this, I believe, is rooted in the differing goals and scientific foundations. The concerns of academic PL are well-addressed by higher mathematics, where the concerns of industrial PL are better answered through disciplines such as organizational psychology. In truth, both are important.
It is my belief that both worlds need to make an effort to get out of their silos. The industrial PL world needs to do a better job at describing the problems it solves and reporting its solutions and findings. The academic PL world needs to acknowledge the intellectual merit of creating real-world realizations of the idealized features presented in academic PL conferences.
Principles of “Industrial Programming Languages”
A first step towards getting out of the silo is to clearly express what the notion of an “industrial programming language” means. This phrase is an example of what might be called a “common-sense” term. Any of my colleagues from OpenJDK certainly could have expounded at length as to its meaning, industrial programmers could probably list a number of examples, and even academics have some notion of what it means (often some variation on “icky details we don’t want to deal with”).
The problem with “common sense” notions is that everyone has their own ideas of what they mean. To effectively study an issue, we must refine such notions into more concrete and unambiguous ideas. A truly principled effort in this direction would, in my opinion, be worthy of peer-reviewed publication. My goal here is merely to begin to explore the ideas.
As a first draft, we can list a number of issues that “industrial” software development must confront, and which “industrial” programming languages must provide tools to address:
- Very large codebases, running from hundreds of thousands to tens of millions of lines of code
- Long-running development, spanning many development cycles and lasting years to decades
- Very large staff headcounts, distributed teams, staff turnover, varying skill-levels
- Withstanding refactoring, architectural changes, and resisting “bit-rot”
- Large and complex APIs, protocols, interfaces, etc, possibly consisting of hundreds of methods/variables
- Interaction with other complex systems, implementation of complex standards and protocols
- Need for highly-configurable systems, large numbers of possible configurations
- Large third-party dependency sets and management thereof
The common theme here is unavoidable complexity and inelegance. It is a well-known fact in many disciplines that different factors emerge and become dominant at different scales. In algorithms and data structures for example, code simplicity is often the dominant factor in execution time at small scales, asymptotic complexity dominates at mid-scale, and I/O cost dominates all other concerns at large scales. Similarly, with software development, certain stresses (such as the ones listed above) emerge and become increasingly important as the scope of a development effort increases.
Industrial practice and industrial languages aim to withstand these factors and the stresses they produce as development scope scales up to modern levels. An important corollary is that the failure to provide mechanisms for dealing with these factors effectively limits the scope of development, as has been the case throughout the development of industrial practice.
Dealing with Development at Scale
I routinely use the term “industrial pragmatics” to refer to the various methods that have been developed in order to cope with the stresses that emerge in large-scale software development. In particular, I use the word “pragmatics” because the efficacy of these techniques generally can’t be effectively evaluated using theory alone. They involve both complex interactions at scale as well as human behavior- two phenomena that defy theoretical abstraction.
It is worth exploring some of these techniques and why they have been so successful.
The Path of Least Eventual Cost/Pain
At very large scales, the only successful strategy for managing things quickly becomes the path of least eventual cost (or for the more blunt, pain). A key word in this is eventual, as it is critically important to realize that some decisions may minimize short-term cost or maximize short-term gain in some way but eventually lead to a much higher cost in the long run. At large scales and in long-running projects, short-sighted decision-making can dramatically increase the eventual cost, to the point of compromising the entire effort.
This is, in my opinion, one of the critically-important principles of industrial pragmatics. Any tool, technique, language, or practice must be evaluated in terms of its effect on eventual cost.
Modularity and Interfaces
More than any other technique, modularity has proven itself invaluable in managing the complexity of industrial-scale software development. The most widely-successful adoption of this technique came in the form of Object-Oriented programming, which removed the barriers that prevented software development from scaling up. Since the advent of OO, other adaptations have emerged: Haskell’s typeclasses, various module systems, and the like, all of which share common features.
A key features of these systems is that they manage complexity by encapsulation- walling off part of a huge and complex system, thereby limiting the concerns of both the author of that component as well as the user. This significant limits the set of concerns developers must address, thereby limiting the size and complexity of any “local” view of the system.
Large systems quickly build up a huge number of interfaces and configurations, and the fraction of possible uses of those interfaces and configurations that represent “valid” or “good” use quickly shrinks to the point where the vast majority of uses are incorrect in some way. Well-designed systems provide mechanisms to restrict or check use of interfaces or configurations to identify misuse, or else restrict use to the “good” cases in some way. Badly designed systems adopt an “anything goes” mentality.
An prime example of this comes in the form of cryptographic APIs. Older crypto APIs (such as OpenSSL) provide a dizzying array of methods that can result in an insecure system at the slightest misuse. This problem was identified in recent academic work, and a series of new crypto APIs that restrict use to correct patterns have been created. Type systems themselves also represent a technology that restricts usage, greatly constraining the space of possible cases and greatly improving the degree to which a program can be analyzed and reasoned about.
Managing Implicit Constraints
In a sufficiently-large system, a significant effort must be dedicated to maintaining knowledge about the system itself and preventing the introduction of flaws by violating the implicit logic of the system. Well-managed systems minimize the externally-facing implicit constraints, expose APIs that further minimize the degree to which they can be violated, and ensure that the unavoidable constraints are easily detected and well-known. Badly-designed systems are rife with such implicit constraints and require expert knowledge in order to avoid them.
This is one area that I believe formal methods can make a huge impact if adapted correctly. There are many ways of approaching this problem: documentation, assertions, unit tests, and so on, but they are all deficient for various reasons. Even the ability to explicitly codify invariants and preconditions would be a considerable boon. More modern languages and tools such as Rust and JML approach this, but only formal methods can provide a truly universal solution.
The Art of API (and Protocol/Standard) Design
The design of APIs is an art that is underappreciated in my opinion. It takes considerable skill to design a good API. It requires the ability to generalize, and more importantly, to know when to generalize and when to hammer down details. It requires the ability to foresee places where people will want to change things and how to make that process easy. It requires a good sense for how people will build upon the API. It requires a good sense of necessary vs. unnecessary complexity. Lastly, It requires a knack for human factors and for designing things to make doing the right thing easy and the wrong thing hard or impossible.
Failure of some kind becomes unavoidable at large scales. Software systems subject to real use will eventually be used incorrectly, and it will become necessary to diagnose failures quickly and efficiently. This is unavoidable, even in a perfect world where all of our own developers are perfect- users and third-party developers can and will do things wrong, and they need to be able to figure out why. In the real world, our own developers also must diagnose failures, if only in the internal development and testing processes.
This, I think, is one of the most undervalued principles in both academic and even industrial circles. Far too many people want to answer the problem of managing failure with “don’t fail”. But failure can’t be avoided or wished away, and failing to provide tools to quickly and effectively diagnose failure translates to increased cost in terms of development times, testing times, and diagnosis of failure in the field (in other words, much more eventual cost and pain).
In my own career, Java and other JVM languages have proven themselves to have the best track record in terms of easy diagnosis of failure of any language I’ve seen in common use, both with myself and with others. By contrast, languages that don’t provide the kind of functionality that JVM languages do, either because they can’t (like C), or because they choose not to (like Haskell) tend to slow things down as it takes longer to diagnose issues. Lastly, I’ve also dealt with some truly nightmarish platforms, such as embedded or boot-loaders, where diagnosis is a task for experts and takes considerable effort and time.
In addition to the principles I’ve discussed thus far, human factors- particularly the difficulty of modifying human behavior -plays a key role in the design of industrial languages. A considerable amount of thought must go into how to influence user behavior and how to get them to adopt new techniques and methodologies, often with little chance of recovering from mistakes. Unlike the other principles, these are rooted in psychology and therefore cannot be the subject of the kinds of mathematical theories that underlie many aspects of PL. They are nonetheless critical to success.
Making it Easy to be Good/Hard to be Bad
One of the most successful principles I’ve learned is that of making it easy to be good and hard to be bad. This means that “good” use of the tool or language should be easy and intuitive, and it should be difficult and non-obvious how to do “bad” things (this of course presupposes an accurate notion of good vs. bad, but that’s another discussion).
An excellent example of this comes from the language Standard ML. Functional programming with immutable data is the notion of “good” in SML, and imperative programming with mutable data is strongly discouraged. It’s tolerated, but the syntax for declaring and using mutable state is gnarly and awkward, thereby encouraging programmers to avoid it in most cases and encapsulate it when they do use it. Java and other languages’ design reflects a notion of object-orientation being “good”, with global state being strongly discouraged and made deliberately difficult to use.
Coordinating human activity at scale is an extremely difficult problem. Regimentation- creating common idioms that serve to make behavior predictable and facilitate implied communication is a very common technique for dealing with the problem at scale. In the context of software development, this takes the form of things like design patterns and anti-patterns, well-defined interfaces and standards, style documents, and programming paradigms.
Languages that succeed at large-scale development tend to provide facilities for this kind of regimentation in one way or another. This incidentally is one major argument in favor of types: they provide a considerable amount of implicit communication between developers and users of an interface. Similarly, languages with well-known idioms and built-in usage patterns tend to produce more coherent codebases. Java is one example of this. Haskell is quite good in some ways (such as its typeclasses, tightly-controlled use of side-effects, and very powerful type system) and deficient in others (five string types). Python achieves good regimentation despite its lack of types, which I believe is a crucial factor in its popularity.
Making Complex Ideas Accessible
A key to success in industrial development is the ability to make a complex idea accessible. In my own experience, this was one of the core design principles of the Lambda project in Java. We had the challenge of introducing higher-order functional programming and all the notions that come along with it in a way that was accessible to programmers used to the stateful OO style of thinking. Conversely, many efforts have gotten this wrong, as exemplified in the infamous quote “a monad is just a monoid in the category of endofunctors”.
This translation between idioms is quite difficult; it requires one to deeply understand both sides of the fence, as well as which use cases and concerns are most common on both sides. However, it’s critical- people don’t use what they can’t understand. The best way to facilitate understanding is to present an idea or principle in a context the audience already understands.
Just as failure must be dealt with in the context of software systems, changing behavior and practices must be dealt with in the context of human factors. As an example, programming practices based on the functional paradigm are becoming increasingly recommended practice due to a number of changing factors in the world. Many languages face the challenge of adapting their user base to these new practices.
The mentality of harm-reduction often proves the most effective attitude when it comes to changing human behavior, both here and elsewhere. Harm-reduction accepts that “bad” behavior takes place and focuses its efforts on minimizing the negative impacts on oneself and others and encouraging a transition towards better behavior in the long-run. This reflects the realities of industrial programming: software can’t be rewritten into a new paradigm all at once, and some legacy systems can’t be eliminated or rewritten at all.
In the design of industrial languages and tools, this takes the form of several adages I’ll list here: provide options instead of demands, minimize upfront costs and facilitate gradual transitions, work with the old but encourage the new.
On Seeming Contradictions
It might seem, particularly to the more academically and philosophically inclined, that many of these principles I’ve elaborated contradict each other. How can we provide regimentation while working with the mentality of harm-reduction? How can we restrict use to the “good” behaviors while gracefully handling failure?
The solution is in itself another critically important principle: the notion of avoiding absolutist conflicts of ideas. In the practical world, ideas tend to be useful in certain contexts, and a given principle needs to be evaluated in the context of use. Put another way, “it’s important to use the right tools for the job”.
On a deeper level, ideological wars tend to end with both sides being “wrong”, and often some synthesis of the two being right. In physics, the debate over whether light was a wave or a particle raged for centuries; in truth, it’s both. There are many other such examples throughout history.
If we reduce everything I’ve discussed down to its essence, we arrive at the following statement: as the scale of industrial programming increases, the dominant concerns become irreducible complexity and inelegance, and human factors associated with coordinating effort. Thus, “industrial pragmatics” refers to a set of techniques and principles for managing these concerns, and industrial programming languages are those languages that consider these techniques in their design.
I have been working on ideas for how to make category theory more accessible and easier to learn, with the belief that it could be eventually be reorganized to the point where it could be taught to high school students interested in math.
I gave a 20-minute talk yesterday at Boston Haskell about the progress of my ideas so far. This stimulated some interesting discussions. I am posting the slides here.