-
Notifications
You must be signed in to change notification settings - Fork 65
Wyvern: A Language for Usable Design Driven Assurance
Wyvern is a new programming language designed from the ground up to support highly productive development of secure software systems. While the language is general purpose, we are especially interested in emerging application areas such as the web, mobile devices, and the internet of things.
Achieving high productivity and high security simultaneously may seem daunting, as there are clear tradeoffs between existing approaches that have been taken to achieve these goals. For example, we could seek to increase security by fully specifying a program's intended behavior and security properties and then verifying the code against that specification, but this could be achieved only at very high cost in programmer time.
The key insight of Wyvern is that we can leapfrog current languages both in productivity and security by providing better support for expressing and enforcing large-scale design. Better support for design is important because design drives the core engineering properties of programs: issues like performance, maintainability, and security, among others. Our observation, grounded in software engineering research and experience, is that as programs grow in scale and complexity, ensuring fidelity to design becomes more critical yet also more difficult. Large programs are by necessity implemented by teams, but making sure that everyone on the team shares a design concept is difficult. Even if everyone knows what the design should be, in the course of implementation engineers may discover that this design needs to change, or may make mistakes in implementing it correctly. Therefore the design of the software as-implemented commonly diverges from the design as-intended, and as a result it fails to realize the critical engineering properties that the design was intended to achieve.
Unfortunately, while modern languages provide good support for expressing the low-level design of algorithms and object structures, they do not provide good support for expressing and enforcing design at larger scales.
Wyvern's goal is to support usable design-driven assurance. Through mechanisms that express and enforce important aspects of large-scale design in a usable way, Wyvern enables architects to build in assurance of the properties most critical to their systems. Examples of expressing and enforcing design include:
-
Hiding information at a scale larger than single modules (e.g. as supported in Standard ML's module system), while also allowing modules to be multiply instantiated and dynamically linked (as is common in Object-Oriented Frameworks).
-
Enforcing architectural constraints such as restricted dependencies between modules [Sullivan et al. 2001], limits on how system resources are used (e.g. as in Google's Caja), or restrictions on the side effects of a task (e.g. as in MapReduce).
-
Expressing designs in notation that is appropriate to a specific domain, such as the layout and style of a user interface (e.g. as in HTML/CSS), or notation that is appropriate to a specific engineering task, such as representing the deployment architecture of a software system.
Important to Wyvern's philosophy is a focus on usability. We eschew full proofs as well as powerful, but difficult-to-use type systems such as information flow types [Myers, 1999]. On the other hand, Wyvern leverages and builds upon now-standard approaches such as type soundness and memory safety that provide assurance and support for design at the low-level.
In addition to these conventional approaches, Wyvern's expression and enforcement of higher-level design properties uses a number of novel lightweight, high-leverage mechanisms:
-
A first-class module system supporting abstract types, building on the DOT type theory underlying Scala but also improving on it via extensions that make typechecking decidable [Mackay et al., 2020].
-
A capability safe language design, supporting a least-privilege approach to security and enabling architects to enforce a number of important design constraints [Melicher et al., 2017].
-
Types that describe immutability and the effects of operations in a highly usable way [Coblenz et al., 2017].
-
Support for modular language extensions as libraries, allowing developers to express design in domain-specific or task-specific notation [Omar et al., 2014].
It would be convenient to modify existing languages to make them better support large-scale design, and indeed some of the work in our research groups (and much excellent work elsewhere) focuses on this goal. However, fundamental limitations of today's languages mean that we cannot solve these problems as add-ons as successfully as if we design a language from scratch. For example, capability-safety is one innovation we are applying in Wyvern. Prior research has explored making existing statically-typed languages capability-safe, but with significant design compromises: the standard libraries have to be redesigned [Mettler et al., 2010], a barrier to use almost as large as adopting a new language. With a newly designed language, we can focus on solutions to the problem that not only solve the problem more elegantly, but also increase usability by staying closer to today's engineering practice.
Furthermore, capability safety is just one example; module systems, extensible notation, and means of reasoning about state are all areas where we believe that a from-scratch language design can make fundamental advances over building on today's languages. Even if we could design one of these on top of a carefully-chosen existing language, these dimensions work together: for example, our module system, our capability safety approach, and our language extension mechanisms each gain from being able to rely on the design of the others. The sum is greater than the parts, and making all of these advances while also dealing with the design mistakes in legacy languages would result in an unusable system.
Wyvern's design benefits from an interdisciplinary perspective. As programming language researchers, we design in deep properties that provide high reasoning leverage, such as supporting transitive immutability [Coblenz et al., 2016] rather than weaker restrictions such as read-only references or final fields. From software engineering we draw an understanding of what issues impact engineering at scale, such as the architectural structure of an application. Human-computer interaction leads us to focus on usability [Coblenz et al., 2017] and ensure that the unique features of Wyvern are motivated by real software development tasks. This perspective enables us to create a language that is usable by humans, yet is also principled in design and will have high-impact on the software development world.
You can find publications and project members at the Wyvern home page.
While this page is intended to motivate and introduce the ideas behind the design of Wyvern, there is much more to say. We will add links here to more detailed information on various aspects of Wyvern's design in the near future, as well as a tutorial.