Stanford Security Seminar
15 March 2016
Words Matter
Language In
Security Engineering
About Me
Chrome Security engineer since 2011
Formerly
Computers Are Languages
More Languages, More Problems
A browser’s job is to parse and interpret utterances, provided by the world’s least trustworthy sources (the internet), from many grammars:
A Linguist’s View Of Software
Ever tried to parse HTML with regular expressions?
Grammar Class | Machine Type |
Regular | Finite state automaton (NFA, DFA) |
Context-free | Non-deterministic finite-state automaton |
Context-sensitive | Linear bounded automaton |
Recursive | Always-halting Turing machine |
Recursively enumerable | Turing machine |
The paranoid linguist’s view of software.
#langsec is the insight that data are utterances that may also be programs that may also be weird machines.
Weird machines are machines that recognize/generate languages on a surprisingly and/or terrifyingly high position on the Chomsky hierarchy.
The Page-Fault Weird Machine (Bangert, Bratus, Shapiro, Smith)
“Any sufficiently complex input is indistinguishable from byte code” for a weird VM.
Language-Theoretic Security
Another example: the printf “little language” is a weird machine, thanks to %n.
Format String Attacks (Newsham)
This machine (main) recognizes machines (arbitrary argv[1]s) that will do whatever they want to your machine (MacBook Pro):
int main(int argc, char **argv) {
char buf[100];
int x;
if(argc != 2)
exit(1);
x = 1;
snprintf(buf, sizeof buf, argv[1]);
buf[sizeof buf - 1] = 0;
printf("buffer (%zu): %s\n", strlen(buf), buf);
printf("x is %d/%#x (@ %p)\n", x, x, &x);
}
Postel Was Wrong (Thomson)
“In general, an implementation should be conservative in its sending behavior, and liberal in its receiving behavior.” — Jon Postel, trying desperately to get the planet-wide language machine to just to boot, let alone actually send anybody’s utterances.
Increasingly, we are turning away from Postel’s Law — out of necessity. Your compiler should detect and reject untrustworthy format specifiers, and your libc shouldn’t implement %n.
chris@goatbeast:~ $ make printf-weird
clang -Wall -Wextra -Werror printf-weird.c -o printf-weird
printf-weird.c:12:29: error: format string is not a string literal (potentially insecure) [-Werror,-Wformat-security]
snprintf(buf, sizeof buf, argv[1]);
^~~~~~~
Input Complexity: TIFF
The TIFF image file format specification describes the file format as serialized structs. Here is part of the ‘baseline’ TIFF definition; see if you can spot the dormant cyber pathogen:
Input Complexity: H.264
“A specification that cannot be fit on one 8.5 x 11 inch piece of paper cannot be understood.” (Mark Ardis)
The H.264 specification is 263 pages. And not of struct definitions or even a BNF grammar, but pseudo-C code. Here is a simple example:
Challenges
So, there’s no hope of migrating to a langsec-approved suite of languages (context-free and regular) anytime soon.
Nor is C++ safe.
So we have an unsafe language, parsing complex inputs, at high speed.
My kind of party!
Coping Strategies
We use all the clang/LLVM sanitizers:
… on a large cluster of machines running fuzzers 24/7
We also use our own base/numerics for safe integer arithmetic. (Everybody needs one. Ours is complete, performant, and open source!)
Performance vs. Security
We can’t use dynamic_cast: RTTI bloats the code, and Chrome is already plenty big.
So how can we safely cast objects with virtual methods?
Static or debug-only checks for dynamic types don’t work. Let’s take a look...
A Thought On Types
wrds_mttr_t
Even in 2016, C programmers believe the word int refers to the mathematical concept integer. Even programmers who should know better, such as kernel programmers. It’s not even (necessarily) defined as modular arithmetic (!).
grep -ri alloc * in your favorite C/C++ codebase.
The C and C++ language specifications leave the behavior of signed ints undefined! (Fun game: Why?)
The words are simply incapable of carrying the concepts we load them with.
Integers are just the beginning...
Typeful Programming (Cardelli)
“…there must be a mechanical way of verifying that type constraints are respected by programs. … laws should be enforceable: unchecked constraining information, while often useful for documentation purposes, cannot be relied upon and is very hard to keep consistent in large software systems. In general, systems should not exhibit constraints that are not actively enforced at the earliest possible moment. In the case of typechecking the earliest moment is at compile-time, although some checks may have to be deferred until run-time. In contrast, some specifications can be neither typechecked nor deferred until run time, and require general theorem-proving (e.g., in verifying the property of being a constant function).
“Another emphasis is on transparent typing. It should be easy for a programmer to predict reliably which programs are going to typecheck.”
Typeful Programming
Cardelli is concerned with reliability, by which he means (part of) what I call security.
The paper is a pragmatic, readable approach to the concept of propositions as types (Wadler); propositions include security guarantees.
The paper and the language it describes, Quest, provide a framework for understanding what we can (and should) expect from the type systems in our real-world programming languages.
An Example: Origins Are Not URLs
Chrome historically represented the web origin concept (Barth) with a class called GURL — overloading the concept of URLs to include origins.
But an origin is not just the (scheme, host, port) sub-tuple of a URL tuple.
An Example: Origins Are Not URLs
Since the origin is the fundamental boundary/isolation mechanism/principal on the web, it’s Kind Of A Big Deal to get the concept right.
Mike West introduced a new url::Origin class, but we are still trying to retrofit the new concept to old code.
But there are other ways in which typeful programming could have helped us avoid problems...
void SavePackage::OnReceivedSavableResourceLinksForCurrentPage(
const std::vector<GURL>& resources_list,
const std::vector<Referrer>& referrers_list,
const std::vector<GURL>& frames_list) {
if (wait_state_ != RESOURCES_LIST)
return;
DCHECK(resources_list.size() == referrers_list.size());
...
if (all_save_items_count_) {
// Put all sub-resources to wait list.
for (int i = 0; i < static_cast<int>(resources_list.size()); ++i) {
const GURL& u = resources_list[i];
DCHECK(u.is_valid());
SaveFileCreateInfo::SaveFileSource save_source = u.SchemeIsFile() ?
SaveFileCreateInfo::SAVE_FILE_FROM_FILE :
SaveFileCreateInfo::SAVE_FILE_FROM_NET;
SaveItem* save_item = new SaveItem(u, referrers_list[i],
this, save_source);
Say What You Mean With Types
One approach to solve that would be to encapsulate the consistency check in the constructor of a new type, or use a std::map.
class SavableResourceLinks { … }
typedef std::map<GURL, Referrer> ResourcesAndReferrers;
Why not? Insufficiently expressive/convenient (de)serialization API for IPC? Programmer didn’t think of it?
Protocols
What Is A Protocol?
protocol : computer language :: pragmatics : natural language
In other words, when the semantics (as opposed to the syntax) of utterances are context-sensitive.
For example: If Alice says SYN/ACK to Bob, Bob can’t understand it unless Bob (a) said SYN to Alice; (b) immediately before.
Interpreting Languages In Isolated Contexts
To change the interpretation context is to change — potentially to reduce — the meaning of what is said. Privilege reduction, privilege separation.
It’s a great idea, and it works.
But, as we saw in the previous section, it trades one language problem (our JavaScript machine might turn out to be a weird machine and allow web content to take over a renderer) for another set of problems: IPC and (painfully optional) run-time type checking!
Handling Protocols Is Run-Time Type Checking
As Cardelli wisely advises, it is strictly less awesome than static type checking.
As the static_cast example showed, it’s not always sufficiently performant.
As the OnReceivedSavableResourceLinksForCurrentPage example showed, it’s not always as convenient or as obvious as it should be.
Ceremonies
Ceremony Design And Analysis (Ellison)
“The concept of ceremony is introduced as an extension of the concept of network protocol, with human nodes alongside computer nodes and with communication links that include UI, human-to-human communication and transfers of physical objects that carry data. What is out-of-band to a protocol is in-band to a ceremony, and therefore subject to design and analysis using variants of the same mature techniques used for the design and analysis of protocols. Ceremonies include all protocols, as well as all applications with a user interface, all workflow and all provisioning scenarios. A secure ceremony is secure against both normal attacks and social engineering. However, some secure protocols imply ceremonies that cannot be made secure.”
Ceremonies And Unwi[tl]{2}ing Participants
If you thought implementing protocol nodes was hard, due to weak run-time typing, you’ll love the challenge of serializing layer 4 data structures and deserializing them at layer 8!
Imagine an RPC endpoint that
Poor Pragmatics
Even if the person reading that understands the RSA cryptosystem, there are 2 problems:
And yet Chrome ‘knows’ that an attack is underway.
The Tower Of Techno-Babel
It’s hard enough if everyone used English. But, they don’t.
Why Are Translation And Internationalization Hard?
We Don’t Even Know What ‘Names’ Are
Falsehoods Programmers Believe About Names (McKenzie)
It goes on...
Visual Language Is Hard, Too
A language is a grammar of symbols — but words are not the only kinds of symbols.
Visual Language Is Crucial, And Complicated
Visual language is powerful, and often overrides words.
“If it’s good enough for Edward Snowden, it’s good enough for me!”
The powerful image outweighs the verbiage.
Conclusion
Security Engineering Is Adversarial Linguistics
We have to talk to every machine, and to every human, truthfully.
Happy Parsing!