Blog Post

Announcing Spectacle – A language for Writing and Checking Formal Specifications in Haskell

Introduction

We are announcing Spectacle, a domain-specific language for writing and checking formal specifications in Haskell. We initially designed Spectacle as a replacement for TLA+ in specifying critical infrastructure at Awake Security, improving areas that we found frustrating while using TLA+. Spectacle places emphasis on incorporating types into specifications and interoperability with Haskell. Open-sourcing Spectacle is a bid to make formal specification more accessible and drive its adoption within the broader Haskell community.

I will outline the motivation for formal specification and its role as a tool in the following section. This is only to introduce readers unfamiliar with TLA+ or specification languages. Readers who are already familiar with these languages can skip directly to the section titled Spectacle.

Formal Specification

Designing an entirely new system or extending an existing one with a significant feature is, more often than not, a difficult and error-prone process. Software is complex, and humans are fallible, so engineers typically have processes in place to aid them in planning their designs. It is not unusual for a design process to be split among several phases to keep things manageable. Suppose a team of engineers approaches system design by dividing it into the following steps:

  • Write up a document outlining the purpose of the new system or feature, known constraints, and a high-level implementation plan.
  • The team discusses the plan so each member can conceptualize how a feature or system needs to function.
  • Members consider where they may have overlooked crucial details and correct discovered flaws early on.
  • A rough, proof-of-concept implementation is sketched out, and if new challenges are discovered, the plans are adjusted.
  • The team iteratively refines the implementation until it is complete.

Programmers gravitate towards thinking about systems as the composition of their discrete components in a hierarchy organized by abstraction level. The approach to system design laid out above is organized similarly, with an initial high-level description of the system preceding its finer implementation details. Using a procedure like this to guide system design is able to aid an engineering team in several ways:

  • Design documents help effectively communicate a “birds-eye view” of the system across the team.
  • Scrutinizing design documents should reveal oversights or errors in a design before it enters an implementation phase.
  • Written design plans are valuable pieces of documentation.

With this in mind, it would seem that this procedure is a natural fit for reasoning about system design. I’d argue that this procedure is acceptable for most kinds of software but has limited mileage, namely:

  • Complex systems have a changing set of constraints depending on their architecture, for example, distributed or concurrent computation. For these systems, engineers need to make architectural choices early on to inform subsequent planning. Capturing these details like this in a high-level document is difficult at best.
  • There are no rigorous checks done between each phase of the process, leaving room for errors or oversights to appear due to the project moving between phases.
  • Security and reliability characteristics highly depend on implementation, making them difficult to understand until later design phases.

The underlying theme across these limitations is that design documents are too far removed from implementation to accommodate complex systems. These kinds of systems require an approach to design that bridges the separation between planning and implementation phases. 

Formal specification is a technique for describing systems and verifying key properties about them through mathematically rigorous reasoning. Specifications are written in formal specification languages which, at a glimpse, resemble programming languages. While these languages sometimes do have some similar features or syntax when compared to a programming language, there are several distinguishing characteristics in a specification language:

  • Formal specification languages have some mathematical system as a foundation, of which temporal logic is perhaps the most widely used.
  • Specifications describe how systems should behave rather than how that behavior takes place or is implemented.
  • Specification languages emphasize unambiguously communicating the intent of the system in minimal terms.

The primary advantage of formal specifications over a design document is that the former has a mathematical system at its core. They allow engineers to ensure that the system described in a specification meets essential requirements. This is typically done by challenging a specification with a property and showing that the behavior captured in a specification can in no way violate that property. Doing this by hand would be an arduous process, though, so specification languages typically provide some form of automatically testing specifications in this way.

TLA+

In the past, we have used TLA+ to verify the correctness and reliability of critical infrastructure at Awake. TLA+ is a formal specification language that is especially suited for specifying the behavior of distributed systems and concurrent computation. In the section on specification languages, I mentioned that the automatic verification of specifications is one of the prime reasons for using them. TLA+ provides this functionality through its temporal logic checker (TLC). Glazing over a significant amount of complexity, the TLC is essentially able to extract the behavior from a specification and draw conclusions about whether the behavior agrees with the constraints placed on the specification. To give an example of what I mean by this, assume we have just finished specifying the behavior for how a clock ticks. To say, “The clock will always eventually rollover from 12 pm to 1 am” is a property we expect the clock’s behavior to follow. TLC can verify if specifications satisfy properties like this, and in the case that our clock behaves correctly, it is said to be “correct with respect to its specification.” TLA+ used in conjunction with the TLC has a demonstrated effectiveness in verifying even the most complex systems. Elastic, for example, has used TLA+ to verify their data replication and cluster management

Despite TLA+ being a more than capable tool for specifying software, we were dissatisfied with it. The language has some quirks which made working with it more annoying than it needs to be:

  • TLA+ has three different types of syntax.
  • Setting up continuous integration and version control for specifications written in TLA+ is tricky.
  • TLA+ is an untyped language. Most developers at Awake use Haskell and expect strong types.

It is not impossible to work around these annoyances, but they are very apparent when using the language. 

A significant drawback that affects not just TLA+, but all specification-based approaches to design, is that they necessitate two copies of a codebase to be maintained. Keeping a version of the codebase in a specification language and a “real world” version written in a programming language incurs a lot of overhead. Furthermore, even if a team can justify this overhead, transliterating a practical implementation from specification can be seen as too error-prone to be worthwhile. 

Spectacle

As mentioned in this post’s introduction, Spectacle is a formal specification language that replaces TLA+ for formally specifying the Haskell software at Awake. In order to be a viable replacement for TLA+, Spectacle had to achieve language feature parity with TLA+ and, furthermore, reduce the overhead associated with integrating specification into the design process. Spectacle reimplements all of the language features found in TLA+ that are necessary for authoring specifications of real-world systems. Spectacle also supports automatically checking specifications through its model checker, analogous to TLA+’s temporal logic checker. A complete list of the features we currently support in Spectacle are:

  • First-order logic including conjunction, disjunction, negation, implication, and equality.
  • Universal and existential quantification.
  • Variable priming and the enabled operator.
  • Temporal operators including always, eventually, infinitely often, and stays as. Additionally, Spectacle has support for the temporal operator “until” which is not included in TLA+. 
  • Unfair, weakly fair, and strong-fair scheduling in the model checker.
  • Stutter-step invariance checking.
  • Checking safety and liveness properties in the model checker.
  • Checking termination conditions in the model checker.

Spectacle’s feature parity with TLA+ is not enough on its own to warrant itself as a replacement. We considered two things early in Spectacle’s design: reducing the overhead associated with using specifications and taking advantage of types in specifications (Spectacle is a type-directed EDSL, much like Servant). Since Spectacle is embedded in Haskell rather than a separate language implementation, specifications can directly interoperate with their corresponding production implementations. A consequence of this is that specifications no longer require separate codebases that must be kept in 1-to-1 correspondence with a production implementation. Furthermore, code that is shared by a specification and implementation doesn’t need to be translated when changes to the specification are made. There are, of course, limitations to how much sharing can take place without compromising either the specification or implementation. Specifications will inevitably require some additional code, but testing this myself, I found the extra effort is similar to that required for setting up a mock test.

The usage of types in Spectacle is easier to demonstrate than it is to explain. To show the usage of types within a specification and as well as demonstrate how Spectacle is used, I’ve written a specification for a naive rate limiter as an example. The first step to writing any specification is to declare what information is necessary to capture the behavior we want to model. The purpose of a rate limiter is to set a bandwidth on the number of messages a client can send over some interval of time. Knowing this, we can directly encode this information into the following types:


data RateLimitConsts = RateLimitConsts
  { -- The interval of time we want to limit messages in.
    window :: Int 
    -- The maximum number of messages we can receive with the set interval.
  , msgLimit :: Int
  }

-- The type of messages only considering their age since the message was received.
newtype Message = Message {msgAge :: Int}
  deriving (Hashable, Show)

-- A declaration of variables in the specification. Read as a variable "msgLog" with type @[Message]@.
type RateLimitSpec = '["msgLog" # [Message]]

The RateLimitSpec type is a type-level list (or signature) declaring the names of variables and their types used in the specification. Types used in a specification’s signature are required to have instances of Show and Hashable. Although nothing would prevent you from including the limiting window and message limit as variables in RateLimitSpec, it’s better to leave constants outside the signature, so the model checker has less information to track. To finish specifying the behavior of the rate limiter, we first need to give an initial action that will define what values the msgLog variable can be initialized to and then specify a next-state action that defines how msgLog can change. The initial state for “msgLog” is straightforward to specify but may look strange at first:


specInit :: Initial RateLimitSpec ()
specInit = do
  -- The variable "msgLog" is defined as the empty list.
  #msgLog `define` return []

There’s a bit to unpack here, so to summarize:

  • Initial RateLimitSpec () says that specInit will specify the initial values for all variables in the specification RateLimitSpec.
  • The #msgLog syntax uses the OverloadedLabels extension to refer to the msgLog variable declared in the specifications signature.
  • define syntax declares the variable on the left-hand side (in this case, #msgLog to be initialized as the empty list. The type of #msgLog is inferred from the specifications signature, so giving some erroneous value on the right-hand side will produce a type error.

specInit only describes what values are considered acceptable states for the rate limiter to begin from. To completely specify the behavior of the rate limiter, we also need to describe how the values of variables in the RateLimitSpec signature can change over time. By “changing over time,” we’re not referring to any concrete notion of time; instead, we’re specifying the smallest execution step our behavior could ever make. It is reasonable to assume that one of these steps would simply be to receive a new message in the rate limiter. Translating this into the specification would look like this:


sendMessage :: Action RateLimitSpec Bool
sendMessage = do
  -- plain #msgLog to retrieve the "old" value of msgLog.
  msgLog <- plain #msgLog
  -- #msgLog .= ... to set a new value to msgLog.
  #msgLog .= return (Message 0 : msgLog)
  return True

Here we retrieve the value of msgLog prior to taking a sendMessage step and use the (.=) syntax to update this value by adding a new message with age 0. For Haskell programmers, this incantation should be reminiscent of using a state monad. Updating the value of msgLog in this way minimally defines what it means to receive a new message. For this definition to limit the number of messages we can receive, it has to be extended with an extra condition that drops messages if we’re already at the quota.

sendMessage ::
  -- -XImplicitParams for passing specification constants.
  (?constants :: RateLimitConsts) =>
  Action RateLimitSpec Bool
sendMessage = do
  -- -XRecordWildcard for bringing the constants "window" and "msgLimit" into scope.
  let RateLimitConsts {..} = ?constants
  msgLog <- plain #msgLog
  #msgLog .= return (Message 0 : msgLog)
  return (length msgLog < msgLimit + 1)

Here the implicit parameter ?constants is only deferring the responsibility of threading a record with our specifications constants to Haskell. Passing the constants into sendMessage explicitly would work just as well. Adding the condition (length msgLog < msgLimit) as the return value for sendMessage, we prevent the message log from accumulating messages after reaching the rate limit. In addition to specifying how messages are limited, there needs to be a defined behavior for removing messages that have left the limiting window.


passTime ::
  (?constants :: RateLimitConsts) =>
  Action RateLimitSpec Bool
passTime = do
  let RateLimitConsts {..} = ?constants
  #msgLog
    .= ( -- Retrieve the current value of "msgLog".
         plain #msgLog
          -- Increment the age of each message.
          <&> map (\msg -> Message (msgAge msg + 1))
          -- Remove any message older than the limiting window from the message log.
          <&> filter (\msg -> msgAge msg <= window)
       )
  return True

passTime will increase the age of messages recorded in msgLog, filtering any messages outside the limiting window.

sendMessage and passTime together completely specify how we expect the rate limiter to behave. The actions sendMessage and passTime, as we’ve defined them thus far, are separate from each other. Describing the behavior of systems as a collection of smaller sub-behaviors is a common practice in authoring specifications. Dividing the behavior of a system into (roughly) its smallest actions allows us to make use of the disjunction connective:

specNext :: 
  (?constants :: RateLimitConsts) =>
  Action RateLimitSpec Bool
specNext =
  -- Either perform a "sendMessage" or "passTime" action
  sendMessage \/ passTime

Joining two disparate actions like this is much more than just a bookkeeping or organizational device. The disjunction here expresses the idea that when our program evolves, it can do so either by recording a new message (if possible) or by increasing the age of each message logged. Starting from a single new message, we can enumerate the ways this system can evolve over two steps by depicting the result of taking each action in a disjunction of many as nodes in a tree:

Trees such as this are what a model checker is inspecting when we verify that our behavior operates with respect to some properties we specify along with it. As an aside, this also illustrates why the temporal logic of actions is particularly well suited for tackling concurrent programs. By specifying concurrent processes as a disjunction of many atomic operations, the model checker can generate every conceivable sequence of operations that the system could perform. In the above figure, each left branch is directed to the result of taking sendMessage action while the right branch is the result of passTime. It takes some imagination but knowing this, we could imagine that the left-most leaf is the state resulting from the rate limiter receiving two messages simultaneously. What happens if the rate limiter receives 100 messages at once, though? It could be that running expanding the tree over more steps reveals that the rate limiter fails to block incoming messages after the limit we set. We need to express the property: “The number of messages in msgLog is always below msgLimit, regardless of what sequence of actions are taken.” The declaration specProp is how this property is translated into Spectacle:

specProp ::
  (?constants :: RateLimitConsts) =>
  Invariant RateLimitSpec Bool
specProp = do
  let RateLimitConsts {..} = ?constants
  always do
    msgLog <- plain #msgLog
    return (length msgLog <= msgLimit)

Here the syntax guarantees there is no way to interleave the sendMessage and passTime such that the length msgLog ever exceeds the msgLimit. In order words, there’s no path along the tree we could trace to reach a point where the rate limiter has accepted more messages than it could handle. 

Together specInit, specNext, and specProp give a complete specification of the rate limiter we initially set out to design. There is a bit of boilerplate necessary before the specification can run through the model checker:

spec ::
  (?constants :: RateLimitConsts) =>
  Specification RateLimitSpec
spec =
  Specification
    { initialAction = specInit
    , nextAction = specNext
    , temporalFormula = specProp
    , terminationFormula = Nothing
    , fairnessConstraint = unfair
    }

check :: IO ()
check = do
  let ?constants = RateLimitConsts 
        { window = 10
        , msgLimit = 5
        }
  defaultInteraction (modelCheck spec)

I’ll elude explaining what defaultInteraction is doing besides saying it is necessary to get a repl-like interface with the model checker. Calling the check function in GHCi will report the following:

Success, model checker satisfied all properties with
 * 4368 distinct states
 * A maximum search depth of 4368
 * A maximum search tree width of 11

This, as promised, has exhaustively searched a tree of states generated by the rate limiter’s behavior and was unable to discover a state that violated the specProp invariant. The rate-limiter specification here is oversimplified and only meant to convey the general idea of using Spectacle. The complete source for this specification, along with several more sophisticated applications of Spectacle, can be found here.

Conclusion

Spectacle makes writing formal specifications with the temporal logic of actions easier by enabling the rigorous verification of programs without committing to language abstractions that sacrifice interoperability with Haskell. Haskell’s type system enables us to eliminate “silliness checks” from our specifications, making them more efficient and easier to maintain. Spectacle does not require you to use a specialized, hobbled IDE. Some implementations can be verified, by Spectacle, to satisfy their specification.

Formal specification is a rich subject, so presenting a whirlwind introduction in an accessible manner is difficult. There are a number of features in Spectacle that could not be mentioned or could only briefly be covered here to keep things digestible. I highly encourage anyone familiar with either Haskell or TLA+ to investigate the Spectacle repository and the example specifications in it.

Subscribe!

If you liked what you just read, subscribe to hear about our threat research and security analysis.

Jacob Leach
Jacob Leach

Software Engineer