blob: e8c706589b38c12287f2a81ada818fb6fb14b2e7 [file] [log] [blame] [view]
# Hermeticity
Hermetic functions (or hermetic methods) are pieces of code that can modify
only local state (including its arguments) to store the result of computation.
They cannot modify global state (including thread-related state like mutexes)
or make actual or virtual system calls (including allocating memory or querying
timers). They can call other hermetic functions but any recursion must be
declaratively finite (so that a worst case stack size requirement can be
computed at compile time) and they cannot invoke user-supplied callbacks.
## Purity
Hermeticity is similar to
[purity](https://en.wikipedia.org/wiki/Pure_function), although the exact
definition of purity [depends on who you
ask](https://twitter.com/radokirov/status/1097325661658570752). While pure
functions are usually defined as without side effects, hermetic functions can
modify its arguments' state (not just modify local variables).
For example, in Go notation, `func pureSort(original []int) (sorted []int)`
could take a slice of `int`s and return *a new slice* containing the elements
in sorted order - the `original` slice is not modified. In comparison, `func
hermeticSort(dst []int, src []int) (dstWasLongEnough bool)` could copy `src`'s
elements (in sorted order) to modify *a caller-supplied slice* `dst`, provided
that `dst` was long enough.
This distinction is somewhat fuzzy if you think of the pass-a-`dst`-slice
mechanism as merely a performance optimization for 'returning' large values via
an out parameter. Still, hermetic *methods* are allowed to modify the receiver
argument's state, which is separate from return values or out parameters.
For example, `func (otp *oneTimePad) Transform(dst []byte, src []byte, atEOF
bool) (nDst int, nSrc int, err error)` could combine a [one-time
pad](https://en.wikipedia.org/wiki/One-time_pad) with an input stream, writing
the result to an output stream. Calling `Transform` performs some compute but
it also updates the receiver `otp`'s state to track how much of the one-time
pad remains after successive calls during streaming I/O. This
[`Transform`](https://pkg.go.dev/golang.org/x/text/transform?tab=doc#Transformer)
method can be hermetic without being pure.
## In-Process Sandboxing
Hermeticity is similar to process-level sandboxing (like Linux's
`SECCOMP_MODE_STRICT` sandbox) but for hermetic functions, both caller and
callee are in the same process. The motivation is the same - to compute on
untrusted data without security-compromising surprises, even if there are bugs
in the computation code - but the mechanism is different.
For `seccomp`, the operating system enforces the restriction (at run-time) and
communication (literally IPC or Inter-Process Communication) is heavyweight,
asynchronous and complex.
For Wuffs, the compiler enforces [memory-safety](/doc/note/memory-safety.md)
(at compile time) and communication (a function call) is lightweight,
synchronous and simple. [Wuffs the Language](/doc/wuffs-the-language.md) is
deliberately unpowerful. There are:
- no mutable global variables,
- no mutable TLS (thread-local storage) variables,
- no `unsafe` keyword,
- no FFI (Foreign Function Interface),
- no user-supplied callbacks,
- no system calls,
- no allocation or de-allocation of memory and
- no panicking or throwing exceptions (including for out-of-memory).
Wuffs is designed for writing hermetic, secure libraries, not complete
programs, and **with less power comes easier proof of safety**.
In comparison to compiling C/C++ code with WebAssembly (which can be restricted
to only compute), both Wuffs and Wasm allow for hermetic libraries within
larger (memory-unsafe) C/C++ programs. The difference is that Wasm lets you
re-use existing C/C++ libraries (albeit with a run-time [performance
penalty](https://kripken.github.io/blog/wasm/2020/07/27/wasmboxc.html)) but
Wuffs performs [on par with C
code](https://github.com/google/wuffs/blob/main/doc/benchmarks.md) (albeit
requiring re-writing those libraries).
## Halting
Wuffs functions are not guaranteed to halt. We do not solve the [Halting
Problem](https://en.wikipedia.org/wiki/Halting_problem). Furthermore, while
there is a difference in theory between a function that doesn't halt and one
that halts in 99 years, in practice there is not. Systems that already need to
cope with the latter can also cope with the former.
## Timing and Other Attacks
Technically, 'hermetic' code can still affect other threads or processes
indirectly: modifying what's in hardware caches, OS page tables or that
spending CPU quota leads to a scheduler switch. Wuffs does not guarantee that
code is safe from timing or speculative execution attacks. Nonetheless, Wuffs
code does not have access to any clocks. Any Wuffs computation on "the current
time" requires the caller to explicitly pass in that information.