8 From Assertions to Security
Almost all programming languages either start with or soon acquire an assertion mechanism. In dynamic languages these are often used to check type-like properties (e.g., is something a number) before proceeding with a computation, but even in statically-typed languages they are used to check properties richer than what the type system permits (e.g., is this number prime, this index is inside the array’s range, etc.). The
Wikipedia article on assertions contains the usual mix of gold and dross.
In this assignment we will build a system of assertions suitable for modern software development. We will use #lang racket except where stated otherwise.
For this homework, you are expected to do the work entirely on your own: you may consult with the course staff only for essential information (clarification of typos/errors, names of library functions, etc.: if in doubt you can always ask). In other words, you will do this in “exam mode”. Though some parts will be more challenging than others, we do believe you can do all the problems in this assignment.
8.1 Part 1: Basic Assertions
We will start by defining a function assert that takes an indication of an assertion and a value, and checks that the value meets that assertion. For simplicity, our assertions will only be one of ’num (for numbers), ’bool (for booleans), ’sym (for symbols), ’str (for strings), and ’any (which matches any value; i.e., it never raises an error).
It might be tempting to think of assert as a function of two arguments. For reasons that will soon become clear, we will instead write assert as a function that only takes one argument, the assertion. This returns a function that consumes the value. If the value passes the assertion, the function returns that value. Otherwise, use the provided raise-assertion-error function to raise an error, using the invalid value and the asserted type (for instance, ’num for numbers).
Concretely:
((assert 'num) 3) → 3 |
((assert 'num) "hi") → error |
((assert 'str) 3) → error |
((assert 'bool) true) → true |
In short, an assertion is an identity function for values that pass it.
In writing assert, you may find it useful to use Racket’s pattern-matcher:
(match ct |
['num …] |
['str …] |
['bool …] |
['sym …]) |
Write and test out this portion thoroughly before advancing. You will find the Racket functions number?, string?, boolean?, and symbol? useful. For testing, we have provided the form test-raises-assertion-error?.
8.2 Part 2: Function Assertions
Most assertion languages have a fatal weakness: they only work on “flat” values, as above. Real programs, however, need to also make assertions about higher-order values like functions and objects. For simplicity, in this assignment, we will focus only on functions, and furthermore, on functions of only one argument. Generalizing from this is important in practice but not essential to understand the basic ideas we are learning.
So, let’s say we want to write an assertion of the form
Hint: to pattern-match against this, use
This assertion actually makes three statements:
That the given value is in fact a function.
That the function expects a number.
That the function produces a string.
(If you are suitably pedantic, you might write that last statement as: That, given a number, if the function produces a value, it will be a string.)
Maybe you can see the problem. We can immediately check whether the given value is a function. However, the function may not be called until much later (if at all); and if called, it may not produce a value (if at all) until even later. Therefore, we can perform only the first check now; the second and third absolutely cannot be performed right now.
Most assertion systems have foundered on this point, and either only check the first of these statements, or don’t even try. However, the
Racket contract system showed that there is an elegant solution to this problem. (Note: you may not use any of Racket’s contract features to implement this homework.) The assertive version of a function is essentially a new function that performs the second check on its argument, calls the original function to produce the expected value, and performs the third check on that value before returning it. That is, if we assert
for the value F, it immediately checks that F is a function, and then effectively produces
(lambda (v) |
((assert R) (f ((assert A) v)))) |
Observe that having assert take only one parameter makes this elegant to write. You will find the Racket function procedure? useful.
Extend your earlier assert with the function case and test it well. For instance, consider writing assertions for functions like add1, string-length, and number->string. When you test, make sure that errors that should be flagged by your assertions are indeed flagged by the assertions, not by the underlying Racket primitives. Make sure you include the “flat” tests from the previous part as well.
8.3 Part 3: Testing Nested Function Assertions
The strategy described above works smoothly even when we have richly nested types. For instance, consider the numeric differentiation operator
from DCIC. Observe that its type has “nested arrows”: it is given there as
((Number -> Number) -> (Number -> Number)) |
Translate the code to Racket as a function named raw-d/dx, then use your assert function to define d/dx as the assertive version, with the assertion
'(-> (-> num num) (-> num num)) |
Now think about testing d/dx. We need to test all the modes of failure, which requires thinking about the many ways there are for this assertion to not succeed. Make sure to not limit your thinking to a particular behavior of d/dx.
Write a comment explaining how many different kinds of violations there can be, and why you came up with that number. (For each kind, of course, there can be many concrete violations: e.g., instead of a number one can use a string, a boolean, a function from symbols to strings, and so on and so forth. That is, each kind has an infinite number of concrete violations.)
Pick three of these cases and write concrete tests confirming that the failure is indeed caught by the assertion system. Don’t just write the testing code; write a comment accompanying each test explaining which failure situation it is testing and how. You can be brief: a sentence should suffice.
Be sure to clearly mark this section in your testing file so we can find it while grading.
8.4 Part 4: Count-Limiting
For security, privacy, financial, and other reasons, we sometimes want to place temporal limits on the use of a service. Sometimes these are hard time limits (e.g., messages disappearing on Snapchat after 24 hours) and sometimes they are virtual counts (e.g., a Web document can only be accessed once; after that, even if the link is stolen, using it does not work).
Above, we have seen the notion of wrapping a function: i.e., creating a new, enclosing function that performs some checks before and/or after invoking the actual function of interest. The wrapped function has the same behavior as the original function if there is no violation. We will use the same idea here. For simplicity we will write these separately from assert, to build up a small “policy language” to control function use.
As a stand-in for the various temporal policies we can create, we will focus on the second kind of restriction above, namely limiting how many times a (wrapped) function can be called. Our policy is expressed as a function limit-calls that takes two parameters: a function (of one argument) and a count (a natural number). This produces a wrapped function whose behavior is exactly the same as the original, until the wrapped function has been called too many times, at which point the wrapper errors:
(define sl/2 (limit-calls string-length 2)) |
(sl/2 "hi") → 2 |
(sl/2 "bye") → 3 |
(sl/2 "hi") → error |
In the error case, use the provided raise-limit-error function.
Observe that these wrappers can compose: for instance, we can write
(limit-calls ((assert '(-> num num)) add1) 2) |
This says that the resulting wrapped function checks for consuming and producing numbers and behaves exactly like add1, but can only be called twice.
After defining limit-calls, you should test its behavior. The test support code provides a test-raises-limit-exceeded-error? form for the error case.
Programming Languages Aside
You might wonder what point there is to wrapping assertions or limiting calls when the original function can still be called directly. We can do this because we are working with a simplified model where everything sits in a single module and at the top-level. In practice, these wrappers are used in conjunction with scope. That is, the original function is hidden inside a module or nested scope and only the wrapped version is made available to a client.
That said, in a security setting, we often want to wrap system primitives (e.g., the network or filesystem). In traditional languages, however, these are available to all modules, so scope would not help! That is, every module has a large amount of power that it obtains for free: this is called “ambient authority” (power that is obtained from the surroundings), and an attacker automatically obtains these powers as well. To avoid this, there is a family of object capability (OCaps) languages that work around this. There are some OCaps languages built from scratch (e.g., E, Pony). But several people have also tried to turn existing languages into OCaps languages. See, for instance, W7 from Scheme; Joe-E, a variant of Java; Emily, a variant of OCaml; Shill, an adaptation of the Unix shell; or Secure EcmaScript (SES) for JavaScript (which is in active commercial use). It would be instructive to build such a language, e.g., using Racket’s #lang feature (though Shill protects the shell, it is actually built atop Racket using macros and #lang), but doing so will take longer than we have time for in this assignment.
8.5 Part 5: Revocation
To drive home the power and functioning of wrappers, let’s build one more kind of access limiter. Sometimes we hand out access to some functionality but later want to take it back. This is called revocation. We will now create a revocation wrapper.
A revocation wrapper returns two values: the wrapped function, and a revoker. Therefore, we’ll represent the return from this wrapper as a structure, defined in the stencil:
(struct revocable (f revoker) #:transparent) |
Define a function make-revocable that consumes a function and creates a revocable version of it. In the returned structure, the f field is the original function, while the revoker field is a thunk (function of no arguments); it turns off access to the wrapped function. Subsequent calls should result in an error, using the provided raise-revocation-error function. For instance,
(define add1-revocable (make-revocable add1)) |
|
(define add1/r (revocable-f add1-revocable)) |
|
(add1/r 3) → 4 |
(add1/r 4) → 5 |
((revocable-revoker add1-revocable)) ;; extract and apply the thunk |
(add1/r 3) → error |
Once again, you should be able to compose these features to create a revocable, count-limited, type-asserted function. Write a simple example and a few tests showing that all these features work in harmony. We have provided a test-raises-revocation-error? form in the test support code.
Observe, again, that if a client is given only the revocable version of a function, once access is revoked, they have no way of using the original functionality. Once again, all we need is to use scope properly to make sure they have access to the right version of the function. In a SMoL language, where static scope works, scope can become a big part of the security story!
8.6 Part 6: Dynamic Scope is Bad
We have argued earlier in the semester that dynamic scope is not only bad for reasoning about programs (by compilers, IDEs, and humans), but also hurts security. Let’s see this in action!
In a separate file, port your count-limiting wrapper to #lang
smol/dyn-scope-is-bad. Most of it should work normally but, depending on how exactly you wrote your code, a bit of it may need to be converted: e.g., add1 and sub1 are not defined in that language so they may need to be implemented.
Now use dynamic scope to violate the security provided by the wrapper. Do confirm that the same violation does not work in statically-scoped #lang racket. (You may assume that you, the attacker, have access to the source for constructing your exploit.)
Turn in your new file showing the violation. You do not need to write test cases; it suffices to have top-level expressions and comments indicating what they demonstrate.
8.7 Starter Code
We’ve set up a GitHub Classroom assignment that contains all necessary stencil code and support code
here.
We’ve provided starter code for your implementation at security.rkt. We’ve also provided a stencil for your test cases at security-tests.rkt, and testing support code at test-support.rkt.
8.8 What To Hand In
You will submit three files for this assignment:
security.rkt, which should be uploaded to the “Code” drop on Gradescope.
security-tests.rkt, which should be uploaded to the “Tests” drop on Gradescope.
Your dynamically-scoped version, which should be uploaded to the “Question” drop on Gradescope.
You may also select the entire assert-sec repository to submit to both drops on Gradescope. You can update your submissions as many times as you want before the deadline.
You can update your submissions as many times as you want before the deadline.