These are notes I took for a talk I gave a two occasions:
Abstract: Decentralized Applications (DApps) atop public blockchains are the very hardest programs to write and audit: they run in an adversarial irreversible public environment; one bug, and someone may lose his shirt, with no recourse. How can we affordably write DApps that can be affordably audited, and reasonably trusted? By making their meaning so clear that misunderstanding becomes harder than understanding. We will use a simple DApp to illustrate how we can achieve clarity. Clarity can solve a lot of problems for Software Security, and beyond. But achieving clarity is no easy feat. Clarity requires a simplicity that cannot happen by accident. Clarity requires having carefully identified the concepts that do matter, and systematically eliminated those that don't. Clarity requires using Domain-Specific Languages that embody this selection of concepts and non-concepts.
Author: François-René Rideau is CEO of Mutual Knowledge Systems and author of the DApp language Glow
Let's play a game of “Spot the Bug”.
Let's consider the simplest possible Decentralized Application (DApp): the closing of a sale.
The intent of the DApp is as follows:
a Buyer and a Seller have agreed to the terms of a sale.
The Seller will sign a title transfer, and the Buyer will pay a price for it in tokens.
The title transfer may be an electronic copy of a legal document,
a transaction on another blockchain, a keycode for a hotel room,
or anything in between, etc.
Because they want the transaction to be trustless, the two participants use a blockchain smart contract to ensure that their interaction will be “atomic”, i.e. all or nothing: either they both cooperate and the transaction happens, or one fails to cooperate and then nothing bad happens to the other participant except wasting a bit of time and a small amount of transaction fees.
The sequence diagram for a successful interaction will be as follows:
How can we implement this DApp with standard development tools, and what kind of errors must we guard against?
Here is a simple smart contract for the closing, written in Solidity, today's most used language for that purpose. Can you spot any bug?
Note how it's only 17-line after compressing things a bit,
but would be more like 35 lines when passed through the prettier program
to comply with common style guidelines.
pragma solidity ^0.8.2; // SPDX-License-Identifier: Apache2.0
contract ClosingBug { // Can you identify the bugs in this contract?
address payable Buyer; address payable Seller;
bytes32 digest; uint price;
constructor(address payable _Buyer, address payable _Seller,
bytes32 _digest, uint _price) payable {
Buyer = _Buyer; Seller = _Seller;
digest = _digest; price = _price;
require(msg.value == price);
}
event SignaturePublished(uint8 v, bytes32 r, bytes32 s);
function sign(uint8 v, bytes32 r, bytes32 s) public payable {
require(Seller == ecrecover(digest, v, r, s));
emit SignaturePublished(v, r, s);
selfdestruct(payable(msg.sender));
}
}
Here is one bug: the contract doesn't release escrowed funds back to the Buyer
if the Seller never cooperates.
The Buyer then loses their tokens without getting anything in exchange.
Here is another more subtle bug: the contract releases the money to the msg.sender,
not the Seller, so anyone can watch the seller's signing message,
change the msg.sender on it to themselves,
re-post the same signature with more GAS to get the funds (or mine it themselves),
and thereby front-run the Seller's transaction.
Fixing these two bugs result in a 24-line contract. Assuming of course you can spot the bugs. That would be 47 lines after pretty-printing. Writing the “same” contract in a straightforward way without cleverness or optimizations would take 69 lines once pretty-printed.
Here is a 17-line JavaScript client for the Buyer side on the same smart contract.
Can you spot any bug?
async function Closing__Buyer (timeoutInBlocks, Buyer, Seller, digest, price) {
const contract = new web3.eth.Contract(Closing.abi);
let txHash;
const contractInstance = await contract
.deploy({data: Closing.bin, arguments: [timeoutInBlocks, Buyer, Seller, digest, price]})
.send({from: Buyer}, (err, transactionHash) => {txHash = transactionHash;})
.on("confirmation");
const receipt = await web3.eth.getTransactionReceipt(txHash);
await notify_other_user(Seller, ["Closing__Buyer", 1, receipt,
[timeoutInBlocks, Buyer, Seller, digest, price]]);
const address = receipt.contractAddress;
const deadline = receipt.blockNumber + timeoutInBlocks;
const event = await contractInstance.once("logs", {toBlock: deadline});
const rv = event.returnValues;
assert (check_signature(Seller, digest, rv.v, rv.r, rv.s));
return rv;
}
Here's one: The Buyer fails to recover funds from the contract if the Seller times out.
Fixing that bug is slightly tricky due to mixing exceptions and async,
but can be done in a few lines of code.
Then you have equivalent code on the Seller, which doubles your code base;
and then you must make sure all these pieces fit perfectly together,
and remain in this perfect fit even as the code evolves.
And for all that price, this approach offers no user-interface during the many minutes that it takes to confirm a blockchain transaction. Cue in suspenseful music in a silent submarine...
Now, let's consider the very same application; but instead of writing it in Solidity, let's write it in Glow, the Domain-Specific Language I'm working on. Can you spot any bug?
@interaction({participants=[Buyer, Seller], assets=[price]})
let closing = (digest : Digest) => {
deposit! Buyer -> price;
@publicly!(Seller) let signature = sign(digest);
withdraw! Buyer <- price;
return signature;
};
The program is still supposed to have a buyer pay a price, initially deposited in escrow, in exchange for a seller signing some closing document, at which point the seller receives the buyer's escrowed payment. Let's go line by line:
Buyer and Seller,
who will transact about some asset named the price.closing, and it takes as parameter
the cryptographic digest of a document, that the Seller will sign electronically.Buyer deposits the agreed-upon price in escrow.Seller is now active and publicly signs the digest.
(Publicly signs, means that first he does it in private, then he publishes the signature,
and finally everyone verifies that it checks out.)Buyer takes the money out of the contract.signature is returned at the end of the interaction.So, did you find the bug?
Here it is: the payment of the price is released to the Buyer instead of the Seller.
But that was pretty obvious when reading aloud what the program was doing, isn't it?
Let's fix that bug. Can you spot a bug now?
#lang glow
@interaction({participants=[Buyer, Seller], assets=[price]})
let closing = (digest : Digest) => {
deposit! Buyer -> price;
@publicly!(Seller) let signature = sign(digest);
withdraw! Seller <- price;
return signature;
};
No? Well, neither can I. The program is so compact, in 8 lines (plus 1 blank),
that there's just no space left for a bug to squeeze in unnoticed.
Each line directly corresponds to some aspect of the above sequence diagram,
except for the return signature
that expresses the Buyer's ultimate interest in the signature.
Any line alteration would lead to a bug so obvious that
either the compiler could catch it, or the human auditor probably will.
Glow is a better language because it impossible for programmers to even write those bugs. Entire classes of bugs that plague other languages are inexpressible in Glow:
The accounts must remain balanced, so you can't leave the deposits and withdrawals unmatched.
It's always clear who is doing what or receiving what, and the language always handles all the details of the checking for you. No mis-attribution or wierd race-condition possible.
You can't publicly return the signature unless it was made publicly available earlier.
The program is still valid if you don't explicitly return the signature, but
this will be noticed when writing the user interface for the Buyer.
The language automatically handles the timeouts, both in the contract and the client, you cannot forget about it, because you don't have to remember about it.
Ah yes, from those 8 lines, you get both the smart contract and the client for both participants. That's a 80-90% reduction in the total amount of code required.
In the future, we can also add a check that every participant gets something in exchange for participation, or the contract is rejected for obviously misdesigned incentives. — This would automatically catch the bug I introduced.
But of course, I am not here merely to promote my current software to you. I want to make a larger point about security and software design.
“There are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies. The first method is far more difficult. It demands the same skill, devotion, insight, and even inspiration as the discovery of the simple physical laws which underlie the complex phenomena of nature.” — C.A.R. Hoare, Turing Award Lecture
Let's call these two approaches “Security through Clarity” and “Security through Obscurity”.
“Security through Obscurity” often justifiably gets a bad rap; still, we ultimately rely on some version of it for e.g. passwords; and when you can amend your program to fix deficiencies faster than your enemies can find them, it might be good enough.
However, in situations where a security breach would be catastrophic, when it's too late to fix your software after it's deployed, then only the first approach will do — Security through Clarity.
The solution to Clarity is to “make things as simple as they can be, but no simpler”.
It's easier to audit a 8-line program than a 80-line program — assuming lines of similar terseness. Simplicity wins! Obviously.
But simplicity is easier said than done. How could we keep programs simple to begin with? It's not like others deliberately try to make their programs more complex, is it?
Simplicity isn't automatic. On the contrary, if it isn't specifically sought, complexity is the default.
This is especially true when management aims at programmer “productivity”, and counts it in terms of lines of code produced and features added, and never in terms of lines of code averted or deleted, of architectural simplification. The incentives are just wrong in any organization that has coding metrics. And often the incentives are not even wrong in organization that fail to measure progress.
And yet, even if you avoid those pitfalls, and are genuinely aiming at simplicity, you need to understand where it comes from.
Abstraction is when your language takes care of a lot details so you don't have to.
It supposes two levels of abstraction:
Usually, the concrete level is given to you: from the hardware you have, its operating system, its environment, and its system programming language.
The abstract level then has to be sufficiently low-level for the programmer to express the concepts that matter to him, yet sufficiently high-level to shield the programmer from the details that don't or shouldn't matter to him.
Language Abstraction is everywhere, and everyone is keen to seek and enjoy its benefits, today, when choosing their programming language.
People have replaced binary code with assembly language. Assembly language with FORTRAN, or COBOL. Those first generation languages were replaced by C, then C++, Java, Python, JavaScript, Haskell.
Though there may not be a clear “winner” across all dimensions, each of these and many other languages can abstract over a lot of details that previous languages were forcing programmers to deal with.
And even in systems programming, Rust is now replacing C and C++, wholly eliminating their catastrophic memory leaks and buffer overflows. Now coming for your Linux kernel!
All these languages provide a relatively small number of language abstractions to choose from. And once you pick one, buy into its entire ecosystem that comes with many libraries; but as the name entails, it remains general purpose.
A General Purpose Language is not tailored to your problems; it can abstract over common issues, like memory safety (or it can fail to). But it can only go so deep in whatever particular issues you have.
Thus, Solidity or JavaScript, as specialized as they may be, couldn't fix the “making participant payment obvious” problem, or the “keeping accounts balanced” problem, or the “handling timeout systematically” problem, or the “keeping the participants' software in synch with the smart contract” problem, as experienced by developers of decentralized applications.
I don't know what domain each of you is working in, but whichever it is, I bet that whatever general-purpose language you use is missing a whole lot of concepts you need.
To bring some abstraction, programmers use libraries. Unhappily, libraries do only half of the job of a proper abstraction.
A proper abstraction does two things:
Only then can the programmer safely enjoy the abstraction.
But libraries are generally leaky: they only do the first part, and not the second.
A good abstraction would do the second part, too. It would have no leak, it would be airtight. In Programming Language lingo, we say they would be a full abstraction.
Leaky abstractions don't protect you. At least not as much. They may help you save on some details at some place, but then get to handle a big mess of details at another place, at which point the mess will be inextricable.
The usual approach to deal with the conceptual leaks, is to maintain an iron discipline all along to prevent the mess: always make sure you use the libraries properly, that you match the openings with closings, that you satisfy all the constraints however subtle, that you follow the protocol down to the letter, that you properly implement your “design patterns”, and... that you never forget to propagate every change to all the places that need to know about it.
But you are fallible. Your team is fallible. Even when your code is 100% correct today, someone will forget one of those places to propagate the change to when they add a feature later.
Discipline works, but Discipline does not scale. Discipline is costly. Perfect discipline is infinitely costly. And so you have to weigh this cost against the gains of the leaky abstraction.
What can you do to improve those odds?
Some modern languages such as Haskell or Scala have expressive typesystems that allow library implementers to also express constraints on the use of their libraries, as types. The language then makes it impossible to misuse the library in a way that violates the types.
In many cases, this is enough indeed to make an abstraction airtight. Often, the abstraction is still leaky: there are some laws to your “monad” or library, that the programmers must manually follow because the type system won't help them. But even then, the abstraction can help a lot: like a boat with a few identified leaks you can afford to bail out, rather than a wreck that is more holes than hull.
Still, what is the way to full abstraction?
The only true approach to full abstraction is language abstraction, where you build a language that can let users express exactly the concepts they need, while not being even able to express any of the details that parasite users of libraries, wherein they can only shoot themselves in the foot at the cost of a lot of repetitive work, with no benefit whatsoever when the entire ordeal can be automated away.
Since today's audience is people interested in security, this should remind you of Meredith Patterson's “Language Theoretic Security”, a.k.a. LangSec
In LangSec, you analyze the behavior of program's interactions with its environment as a language in which the environment issues programs that the program evaluates.
Network I/O is a language. User interactions constitute a language. Every program is a language to its users!
Now, for most programs, that language is very simple, and only allows for simple questions and answers, wherein the user configures a few knobs, and the program executes a simple request in response. But other programs offer more control to their users, with a richer language. And the more powerful that language, the more the environment controls you. That might be exactly what's wanted when the program is indeed a language implementation, targeting a local authenticated user as a master to serve. But this is exactly the wrong thing when the program is a public server on the Internet, and offering a universal (“Turing-equivalent”) language to a random connected adversary is essentially being p0wned by them.
But understanding that every program is a language is not just for analysis. It's also for synthesis: write every program as if it were a programming language — because it is.
There is an entire school of programming that thinks kind of this way: the solution to write a program is to design and implement a Domain-Specific Language (DSL) that would be the ideal language in which to write the program, at which point the program because very simple to write, to test, and to audit, with much fewer lines of code and weeks of efforts, — because you only need to deal the the concepts that matter, unhindered by the details that don't.
That's an approach that is actually popular in a large fraction of the users of many programming languages such as FORTH, LISP, APL or Scheme.
But if every program is a language, then every language in which to write a program has to be not just a language but a language-implementation language, with language-implementation tools. None take this “Language-Oriented Programming” story as serious as the Racket community. I personally am using Gerbil Scheme, a close cousin of Racket, with some advantages for my particular use case, though disadvantages for other use cases.
In Racket, and to a point in Scheme and other Lisp languages, you don't just build one abstract computation on top of a more concrete one; you build towers of abstractions, where each floor (but the last?) is itself the ceiling of further lower-level abstraction. Below, there is nothing but turtles all the way down; above, it's towers all the way up. Language abstractions built on top of language abstractions.
Interestingly, some, even most, of these language abstractions may leak; yet, as long as they are part of implementing a simple enough DSL that doesn't leak, the overall design won't leak, and can isolate the application complexity from the implementation complexity, with a language abstraction in-between. In other words, it's easier to maintain the discipline of dealing with leaky abstractions when these leaky abstractions are part of a small project that will have a small amount of leakage to deal with, and that itself won't leak details in or out.
These questions need not have the same answer.
If you need something done tomorrow that will be thrown away next week, pick whichever language is at hand.
For a project with a 1-year horizon, pick a popular tool of the day.
But for a project with a 10-year horizon or beyond, maybe you should think strategically. Never thinking about the long-term is a good way of ensuring you will never have long-term to think about. At the same time, Systemantics teaches us that large systems that run always start as small systems that run, that grow, and that never stop to run as they grow.
I can't convince people who are not interested in the long run. I can only convince people who are interested in the long run to consider concepts they might never have even exposed to: that there is a better way to organize software in the long run than most people imagine.
Once you accept that fact, then you realize you will have to write software differently — but also to rewrite your existing software to be better architected and safer. And you may have millions of lines of code, maybe even hundreds of millions, to deal with.
Happily, you do not have to migrate your entire codebase at once. You can do it incrementally, and you should prioritize.
Clarity is not just for the Security of your Software. It is also for the Security of your wetware against attacks.
If in any matter you don't pick the simplest explanation, then you are letting someone else manipulate you — whoever inserts the extra details. And if there is some way in which you are systematically eschewing the simplest explanation, then you are letting someone else systematically manipulate you.
That is why the approach of Security through Clarity applies to all venues of life. It is an important concept of epistemology. It has been said of a philosopher I like that she had a knack for Reductio ad claritatem — reduction to clarity. We should strive in our life in general to achieve this clarity in our thoughts. That is hard. But the effort is worth it.