Wyvern: Improving
Architecture-Based Security
via a Programming Language
A/Prof Alex Potanin

1Software Security isa Big Problem

2

Why Systems areVulnerable?
We "know" how to code securely
Follow the rules: CERT, Oracle, ...
Technical advances: types, memory safety
But we still fail too often!
Root causes
Coding instead of engineering
Human limitations
Unusable tools3

Our Approach: Usable
Architecture-Based Security
Secure systems
development

Engineering:Usability:

An architecture/design

A human perspective

perspective

λFormal Modelling: A mathematical perspective
4

The WyvernProgramming Language
Designed for security andproductivity from the ground up
General purpose, but emphasisingweb, mobile, and IoT apps
http://wyvernlang.github.io/

5

The Wyvern
Programming Language
But you might ask: "Isn't there a trade
off between security and productivity?

Security

Productivity

What is Wyvern's secret sauce?
6

7

Shifting theTradeoff Curve
Better expressing and enforcing design could
fundamentally shift the tradeoff curve

Security

Productivity

8

Wyvern
Design goals
Sound, modern language design
Type- and memory- safe, mostly
functional, advanced module system
Incorporate usability principles
Security mechanisms built in9

Hello, world!

require stdout
stdout.print("Hello, world!\n")10

SQL CommandInjection

11

SQL Injection: aSolved Problem?
PreparedStatement s = connection.prepareStatement("SELECT * FROM Students WHERE name = ?;");
s.setString(1, userName);s.executeQuery();
Fill the hole

Prepare a statement

securelywith a hole

Evaluation
Usability: unnatural, verbose

λDesign: string manipulation captures domain poorly
Language semantics: largely lost - just strings
No type checking, IDE services, ...
12Wyvern: Usable
Secure Programming
A SQL query in Wyvern:connection.executeQuery(~)~ introduces a domainspecific language (DSL) on thenext indented lines

SELECT * FROM Students WHERE name = {studentName}
Semantically rich DSL. Can provide type

Safely incorporates dynamic data -checking, syntax highlighting, autocomplete, ...

as data, not a command

Claim: the secure version more naturaland more usable
No empirical evaluation, yet13

Technical Challenge:
Syntax Conflicts

λLanguage extensions as libraries has been tried
beforeExample: SugarJ/Sugar* [Erdweg et al, 2010; 2013]
Is it XML or HTML?

import XML, HTMLval snippet = ~How do I <b>parse</b> this example?

14

Syntax Conflicts:
Wyvern's Solution
metadata keyword indicates we areimporting syntax, not just a library

import metadata XML, HTMLNo ambiguity: the compiler loads the uniqueparser associated with the expected type XML

val snippet : XML = ~How do I <b>parse</b> this example?
Syntax of language completely unrestricted indentation separates from host language
15Technical Challenge:
Semantics
Q: Is it safe to run custom parser at compile time?

λA: Yes - immutability types used to ensure imported
metadata is purely functional, has no network access, etc.
Language definition includes

import metadata SQL
custom type checker - can verify
val connection = SQL.connect(...) query against database schema
val studentName = input(...)
connection.executeQuery(~)
SELECT * FROM Students WHERE name = {studentName}

Splicing (as in genes) theory ensures

SQL extension has access tocapture-avoiding substitution invariables and their types incode generated by SQL extension -Wyvern host language

safe to use host language variables
1617How do you enterand exit a TSL?
In the base language, several inline delimiters
can be used to create a TSL literal:If you use the block delimiter tilde (~), there are
no restrictions on the subsequent TSL literal.
Indentation ("layout") determines the end ofthe block18

How do you associatea TSL with a type?

19

Why not associate agrammar with a type?

20

TSL Benefits
Modularity and Safe Composability
Identifiability (easily see which DSL
due to expected type)
SimplicityFlexibility (whitespace delimited
blocks => arbitrary syntax)
21

TSL Limitations

Decidability of Compilation
No editor support (coming?)

22

Our Approach: Usable
Architecture-Based Security
DSL support in
WyvernEngineering:Usability:

Express design in

Natural syntax, enablingdomain-specific way

IDE support

λFormal Modelling: Type safety, variable hygiene, conflict-free extensions
23

An Old Idea:
Layered Architectures[Dijkstra 1968]

Lowest layer: an unsafe, low-level
library

Application CodeMiddle layer: a higher-levelframework
Top layer: the application
Code must obey strict layeringSafe high-level framework

Many variants:
Secure networking framework
Safe SQL-access library

Unsafe low-level library

Replicated storage library
RQ: Can we use capabilities to enforce layered resource access?
* Capability: an unforgeable token controlling access to a resource [Dennis & Van Horn 1966]24

Architecture: Principleof Least Privilege (PoLP)
Every module must be able toaccess only the resources
necessary for its legitimate
purpose [Saltzer & Schroeder
75]
Architectural layering example:
Only Safe SQL library mayaccess the low-level SQL
interface25

All other application code

Safe SQL DSL Library

String-based SQL LibraryModule Linking as
Architecture
require db.stringSQL

To access external resources like a database,main requires a capability from the run-timesystem. A capability is an unforgeable token
controlling access to a resource.

stringSQL

application.run()26

Module Linking as
Architecture
We can import code modules, but they have noambient authority to access resources (cf Newspeak).
sqlApplication cannot access the database by itself.
require db.stringSQL

import db.safeSQL
import app.sqlApplication

safeSQL

val sql = safeSQL(stringSQL)
val application = sqlApplication(sql)stringSQL

application.run()

We must instantiate a sqlApplication object, passing it
the resources it needs. We pass only a capability to
the safe library.
27

Module Linking asArchitecture
module def sqlApplication(safeSQL : db.SafeSQL)
def run() : Int// application code

sqlApplication

require db.stringSQL

import db.safeSQL
import app.sqlApplication

safeSQL

val sql = safeSQL(stringSQL)
val application = sqlApplication(sql)stringSQL

application.run()module def safeSQL(strSQL : db.StringSQL)// implement ADT in terms of strings
28How Hard to Link it
All Up?
Most Wyvern modules don't have state, can be freely imported

Provides accessto OS resource

Statically tracked: stateful modules/objects and resource types

resource type Filedef write(s : String)type SetM
resource type Set
Type of modules is pure; no static state. Objects
def add(v : Int)
def isMember(v : Int) : Bool created by module may be stateful resources, though.
def makeSet() : Set
module setM : SetM
Resources must be passed in; puremodule def client(aFile : File)
import setM ...

modules can just be imported.

resource types capture state or system access: other types do not
Useful design documentation; e.g. MapReduce tasks should be statelessSupports powerful equational reasoning, safe concurrency, etc.

29

Checking PoLP withEffects// in signature of the rawSQL module

The unsafe SQL library defines
an UnsafeSQL effecteffect UnsafeQuery
type Connection

Query operations have anUnsafeQuery effectdef connect(...) : Connection
def query(q:String) : {UnsafeQuery} DataError: getData() must declareeffect rawSQL.UnsafeQuery// client codedef getData(input : String) : DatarawSQL.query("SELECT * FROM Students WHERE name = '" + input + "';")

NB! In Wyvern Effect is a
"Resource.Operation" pair.

Has effect rawSQL.UnsafeQuery30

Checking PoLP withEffects// in signature of the rawSQL module

The unsafe SQL library defines
an UnsafeSQL effecteffect UnsafeQuery
type Connection

Query operations have anUnsafeQuery effectdef connect(...) : Connection
def query(q:String) : {UnsafeQuery} Data

All dangerous code markedwith effect// client codedef getData(input : String) : {rawSQL.UnsafeQuery} Data

rawSQL.query("SELECT * FROM Students WHERE name = '" + input + "';")

NB! In Wyvern Effect is a
"Resource.Operation" pair.

Has effect rawSQL.UnsafeQuery
31

Effect Abstraction
Issue: won't users of the safeSQL library have an UnsafeQueryeffect, if safe SQL is built on rawSQL?

The safeSQL functor
uses a rawSQL module

module def safeSQL(rawSQL : RawSQL) : SafeSQLtype SQLmetadata ...

Defines a SQL ADT withmetadata for parsing

abstract effect SafeQuery = rawSQL.UnsafeQuerydef query(SQL) : {SafeQuery} Data...

Now clients have effectsafeSQL.SafeQueryThe SafeQuery effect isdefined in terms of
UnsafeQuery. Thisdefinition is abstract hidden from clients.

Q: Can't any library do this, potentially hiding unsafe queries?
A: Potentially, but can mechanically check only trusted libraries do so32

Effect SystemUsability
Isn't it a pain to declare all these effects?

Client CodeSafe SQL DSL Library

Case in point: exception specifications in JavaWe can bound a module's effects by its capabilities
No need to effect-annotate the module
Does assume capability-safety (cf JS Frozen Realms)
Client can have effectsafeSQL.SafeQuery (and nothing else)

module def client(safeSQL : SafeSQL) : Client
import ...

If safeSQL defines higher-order functions, makesure the argument is allowed to have theImports may not be
resources - no effects.

SafeQuery effect (cf contravariant subtyping).
33

Wyvern Effects
ExampleNot Annotated
AnnotatedEditor

uses

uses

usesLogger

Configured to log either toa file or a network
34PluginImporting Effect
Unannotated Code35

Importing Effect
Unannotated Code36

Importing Effect
Unannotated Code37

Importing Effect
Unannotated Code38

Importing Effect
Unannotated Code39

Our Approach: Usable
Architecture-Based Security
Effects andcapabilities inWyvern
Engineering:Usability:

Architectural restrictions

Bound effects based onon resource use

architecture

λFormal Modelling: effect- and capability- safety, effect bounds
40Questions?

41