Puffs is a domain-specific language and library for parsing untrusted file formats safely. Examples of such file formats include images, audio, video, fonts and compressed archives.
Unlike the C programming language, Puffs is safe with respect to buffer overflows, integer arithmetic overflows and null pointer dereferences. The key difference between Puffs and other memory-safe languages is that all such checks are done at compile time, not at run time. If it compiles, it is safe, with respect to those three bug classes.
The aim is to produce software libraries that are as safe as Go or Rust, roughly speaking, but as fast as C, and that can be used anywhere C libraries are used. This includes very large C/C++ products, such as popular web browsers and operating systems (using that term to include desktop and mobile user interfaces, not just the kernel).
The trade-off in aiming for both safety and speed is that Puffs programs take
longer for a programmer to write, as they have to explicitly annotate their
programs with proofs of safety. A statement like x += 1 unsurprisingly means
to increment the variable x by 1. However, in Puffs, such a statement is a
compile time error unless the compiler can also prove that x is not the
maximal value of x's type (e.g. x is not 255 if x is a u8), as the
increment would otherwise overflow. Similarly, an integer arithmetic expression
like x / y is a compile time error unless the compiler can also prove that
y is not zero.
Puffs is not a general purpose programming language. While technically possible, it is unlikely that a Puffs compiler would be worth writing in Puffs.
The std/gif/decode_lzw.puffs file is a good
example. See the "Poking Around" section below for more guidance.
For example, making this one-line edit to the GIF codec leads to a compile time
error. puffs gen fails to generate the C code, i.e. fails to compile
(transpile) the Puffs code to C code:
$ git diff
diff --git a/std/gif/decode_lzw.puffs b/std/gif/decode_lzw.puffs
index f878c5e..f10dcee 100644
--- a/std/gif/decode_lzw.puffs
+++ b/std/gif/decode_lzw.puffs
@@ -98,7 +98,7 @@ pub func lzw_decoder.decode?(dst ptr buf1, src ptr buf1, src_final bool)() {
in.dst.write?(x:s)
if use_save_code {
- this.suffixes[save_code] = c as u8
+ this.suffixes[save_code] = (c + 1) as u8
this.prefixes[save_code] = prev_code as u16
}
$ puffs gen std/gif
check: expression "(c + 1) as u8" bounds [1..256] is not within bounds [0..255] at
/home/n/go/src/github.com/google/puffs/std/gif/decode_lzw.puffs:101. Facts:
n_bits < 8
c < 256
this.stack[s] == (c as u8)
use_save_code
In comparison, this two-line edit will compile (but the "does it decode GIF correctly" tests then fail):
$ git diff
diff --git a/std/gif/decode_lzw.puffs b/std/gif/decode_lzw.puffs
index f878c5e..b43443d 100644
--- a/std/gif/decode_lzw.puffs
+++ b/std/gif/decode_lzw.puffs
@@ -97,8 +97,8 @@ pub func lzw_decoder.decode?(dst ptr buf1, src ptr buf1, src_final bool)() {
// type checking, bounds checking and code generation for it).
in.dst.write?(x:s)
- if use_save_code {
- this.suffixes[save_code] = c as u8
+ if use_save_code and (c < 200) {
+ this.suffixes[save_code] = (c + 1) as u8
this.prefixes[save_code] = prev_code as u16
}
$ puffs gen std/gif
gen wrote: /home/n/go/src/github.com/google/puffs/gen/c/gif.c
gen unchanged: /home/n/go/src/github.com/google/puffs/gen/h/gif.h
$ puffs test std/gif
gen unchanged: /home/n/go/src/github.com/google/puffs/gen/c/gif.c
gen unchanged: /home/n/go/src/github.com/google/puffs/gen/h/gif.h
test: /home/n/go/src/github.com/google/puffs/test/c/gif
gif/basic.c clang PASS (8 tests run)
gif/basic.c gcc PASS (8 tests run)
gif/gif.c clang FAIL test_lzw_decode: bufs1_equal: wi: got 19311, want 19200.
contents differ at byte 3 (in hex: 0x000003):
000000: dcdc dc00 00d9 f5f9 f6df dc5f 393a 3a3a ..........._9:::
000010: 3a3b 618e c8e4 e4e4 e5e4 e600 00e4 bbbb :;a.............
000020: eded 8f91 9191 9090 9090 9190 9192 9192 ................
000030: 9191 9292 9191 9293 93f0 f0f0 f1f1 f2f2 ................
excerpts of got (above) versus want (below):
000000: dcdc dcdc dcd9 f5f9 f6df dc5f 393a 3a3a ..........._9:::
000010: 3a3a 618e c8e4 e4e4 e5e4 e6e4 e4e4 bbbb ::a.............
000020: eded 8f91 9191 9090 9090 9090 9191 9191 ................
000030: 9191 9191 9191 9193 93f0 f0f0 f1f1 f2f2 ................
gif/gif.c gcc FAIL test_lzw_decode: bufs1_equal: wi: got 19311, want 19200.
contents differ at byte 3 (in hex: 0x000003):
000000: dcdc dc00 00d9 f5f9 f6df dc5f 393a 3a3a ..........._9:::
000010: 3a3b 618e c8e4 e4e4 e5e4 e600 00e4 bbbb :;a.............
000020: eded 8f91 9191 9090 9090 9190 9192 9192 ................
000030: 9191 9292 9191 9293 93f0 f0f0 f1f1 f2f2 ................
excerpts of got (above) versus want (below):
000000: dcdc dcdc dcd9 f5f9 f6df dc5f 393a 3a3a ..........._9:::
000010: 3a3a 618e c8e4 e4e4 e5e4 e6e4 e4e4 bbbb ::a.............
000020: eded 8f91 9191 9090 9090 9090 9191 9191 ................
000030: 9191 9191 9191 9193 93f0 f0f0 f1f1 f2f2 ................
puffs-test-c: some tests failed
puffs test: some tests failed
Parsing untrusted data, such as images downloaded from across the web, have a long history of security vulnerabilities. As of 2017, libpng is over 18 years old, and the PNG specification is dated 2003, but that well examined C library is still getting CVE's published in 2017.
Sandboxing and fuzzing can mitigate the danger, but they are reactions to C's fundamental unsafety. Newer programming languages remove entire classes of potential security bugs. Buffer overflows and null pointer dereferences are amongst the most well known.
Less well known are integer overflow bugs. Offset-length pairs, defining a
sub-section of a file, are seen in many file formats, such as OpenType fonts
and PDF documents. A conscientious C programmer might think to check that a
section of a file or a buffer is within bounds by writing if (offset + length < end) before processing that section, but that addition can silently
overflow, and a maliciously crafted file might bypass the check.
A variation on this theme is where offset is a pointer, exemplified by
capnproto's
CVE-2017-7892
and another
example.
For a pointer-typed offset, witnessing such a vulnerability can depend on both
the malicious input itself and the addresses of the memory the software used to
process that input. Those addresses can vary from run to run and from system to
system, e.g. 32-bit versus 64-bit systems and whether dynamically allocated
memory can have sufficiently high address values, and that variability makes it
harder to reproduce and to catch such subtle bugs from fuzzing.
In C, some integer overflow is undefined behavior, as per the C99 spec section 3.4.3. In Go, integer overflow is silently ignored. In Rust, integer overflow is checked at run time in debug mode and silently ignored in release mode by default, as the run time performance penalty was deemed too great. In Swift, it's a run time error. In D, it's configurable. Other languages like Python and Haskell can automatically spill into 'big integers' larger than 64 bits, but this can have a performance impact when such integers are used in inner loops.
Even if overflow is checked, it is usually checked at run time. Similarly,
modern languages do their bounds checking at run time. An expression like
a[i] is really if ((0 <= i) && (i < a.length)) { use a[i] } else { throw },
in mangled pseudo-code. Compilers for these languages can often eliminate many
of these bounds checks, e.g. if i is an iterator index, but not always all of
them.
The run time cost is small, measured in nanoseconds. But if an image decoding library has to eat this cost per pixel, and you have a megapixel image, then nanoseconds become milliseconds, and milliseconds can matter.
In comparison, in Puffs, all bounds checks and arithmetic overflow checks happen at compile time, with zero run time overhead.
Puffs code (that is proved safe via explicit assertions) is compiled to C code
(with those assertions removed) - it is transpiled. If you are a C/C++
programmer and just want to use the C edition of the Puffs standard library,
then clone the repository and look at the files in the gen/c and gen/h
directories. No other software tools are required and there are no library
dependencies, other than C standard library concepts like <stdint.h>'s
uint32_t type and <string.h>'s memset function.
If your C/C++ project is large, you might want both the .c files (adding each
to your build system) and the .h files. If your C/C++ project is small, you
might only need the .c files, not the .h files, as the .c files are designed to
be a drop-in library.
For example, if you want a GIF decoder, you only need gif.c. See TODO for an
example. More complicated decoders might require multiple .c files - multiple
modules. For example, the PNG codec (TODO) requires the flate codec, but they
are separate files, since HTTP can use also flate compression (also known as
gzip or zlib, roughly speaking) without necessarily processing PNG images.
If you want to modify the Puffs standard library, or compile your own Puffs code, you will need to do a little more work, and will have to install at least the Go toolchain in order to build the Puffs tools. To run the test suite, you might also have to install C compilers like clang and gcc, as well as C libraries (and their .h files) like libjpeg and libpng, as some tests compare that Puffs produces exactly the same output as these other libraries.
Running go get -v github.com/google/puffs/cmd/... will download and install
the Puffs tools. Change get to install to re-install those programs without
downloading, e.g. after you've modified their source code, or after a manually
issued git pull. The Puffs tools that you'll most often use are puffsfmt
(analogous to clang-format, gofmt or rustfmt) and puffs (roughly
analogous to make, go or cargo).
You should now be able to run puffs test. If all goes well, you should see
some output containing the word "PASS" multiple times.
Feel free to edit the std/gif/decode_lzw.puffs file, which implements the GIF
LZW decoder. After editing, run puffs gen std/gif or puffs test std/gif to
re-generate the C edition of the Puffs standard library's GIF codec, and
optionally run its tests.
Try deleting an assert statement and re-running puffs gen. The result should
be syntactically valid, but a compile error, as some bounds checks can no
longer be proven.
Find the line var bits u32, which declares the bits variable and initializes
it to zero. Try adding bits -= 1 on a new line of code after it. Again,
puffs gen should fail, as the computation can underflow.
Similarly, replacing the line var n_bits u32 with var n_bits u32 = 10
should fail, as an n_bits < 8 assertion, a pre-condition, a few lines further
down again cannot be proven.
Similarly, changing the 4095 in var prev_code u32[..4095] either higher or
lower should fail.
Try adding assert false at various places, which should obviously fail, but
should also cause puffs gen to print what facts the compiler can prove at
that point. This can be useful when debugging why Puffs can't prove something
you think it should be able to.
If you've changed any of the tools (i.e. changed any .go code), re-run go install -v github.com/google/puffs/cmd/... and go test github.com/google/puffs/lang/....
If you've changed any of the libraries (i.e. changed any .puffs code), run
puffs test or, ideally, puffs test -mimic to also check that Puffs' output
mimics (i.e. exactly matches) other libraries' output, such as giflib for GIF,
libpng for PNG, etc.
If your library change is an optimization, run puffs bench or puffs bench -mimic both before and after your change to quantify the improvement. The
mimic benchmark numbers should't change if you're only changing .puffs code,
but seeing zero change in those numbers is a sanity check on any unrelated
system variance, such as software updates or virus checkers running in the
background.
langholds the Go libraries that implement the Puffs language: tokenizer, AST, parser, renderer, etc. The Puffs tools are written in Go, but as mentioned above, Puffs transpiles to C code, and Go is not necessarily involved if all you want is to use the C edition of Puffs.cmdholds Puffs' command line tools, also written in Go.stdholds the Puffs standard library's code. The initial focus is on popular image codecs: BMP, GIF, JPEG, PNG, TIFF and WEBP.genholds the transpiled editions of that standard library. The initial focus is generating C code. Later on, the repository might include generated Go and Rust code.testholds the tests for the Puffs standard library.scriptholds miscellaneous utility programs.docholds documentation.exampleholds example programs.
For a guide on how various things work together, the "99ff8e2 Let fields have default values" commit is an example of adding new Puffs syntax and threading that all the way through to C code generation and testing.
- Puffs the Language
- Puffs the Library (TODO)
- Related Work
- Roadmap
Measurements:
Proof of concept. Version 0.1 at best. API and ABI aren't stabilized yet. There are plenty of tests to create, docs to write and TODOs to do. The compiler undoubtedly has bugs. Assertion checking needs more rigor, especially around side effects and aliasing, and being sufficiently well specified to allow alternative implementations. Lots of detail needs work, but the broad brushstrokes are there.
The mailing list is at https://groups.google.com/forum/#!forum/puffslang.
The CONTRIBUTING.md file contains instructions on how to file the Contributor License Agreement before sending any pull requests (PRs). Of course, if you're new to the project, it's usually best to discuss any proposals and reach consensus before sending your first PR.
Apache 2. See the LICENSE file for details.
This is not an official Google product, it is just code that happens to be owned by Google.
Updated on November 2017.