# HG changeset patch # User Christian Urban # Date 1418022868 0 # Node ID 5a6e8b7d20f712f9cac0ee20b0e998a262368409 # Parent 7f0ac1355f0b9d896e70e1e87855e5317955eee0 updated diff -r 7f0ac1355f0b -r 5a6e8b7d20f7 handouts/ho08.pdf Binary file handouts/ho08.pdf has changed diff -r 7f0ac1355f0b -r 5a6e8b7d20f7 handouts/ho08.tex --- a/handouts/ho08.tex Fri Dec 05 01:17:31 2014 +0000 +++ b/handouts/ho08.tex Mon Dec 08 07:14:28 2014 +0000 @@ -81,7 +81,7 @@ Gmail, but which are always already taken. One major difference between Bitcoins and traditional banking -is that you do not have a place, or places, that record the +is that you do not have a place, or few places, that record the balance on your account. Traditional banking involves a central ledger which specifies the current balance in each account, for example @@ -118,7 +118,7 @@ Did Alice intend to send him 10 Bitcoins, or did the message get duplicated by for example an attacker re-playing a sniffed message? What is needed is a kind of serial number for such -transactions. This means transaction messages look more like +transactions. This means transaction messages shoul look more like \begin{center} $\{\text{I, Alice, am giving Bob Bitcoin \#1234567.}\}_{K^{priv}_{Alice}}$ @@ -216,7 +216,7 @@ In Bitcoins you have the ability to both combine incoming transactions, but also to split outgoing transactions to -potentially more than one receiver. The latter is needed. +potentially more than one receiver. The latter is also needed. Consider again the rightmost transactions in Figure~\ref{txngraph} and suppose Alice is a coffeeshop owner selling coffees for 1 Bitcoin. Charles received a transaction @@ -323,7 +323,7 @@ The reflex reaction to such a situation would be to make the process of validating a transaction as cheap as possible. The -intention is that Bob will get enough peers to agree with him +intention is that Bob will easily get enough peers to agree with him that he is the rightful owner. But such a solution has always the limitation of Alice setting up an even bigger network of puppy identities. The really cool idea of Bitcoin is to go @@ -419,7 +419,7 @@ \label{unconfirmed} \end{equation} -\noindent The puzzle is given as follows: There are some +\noindent The puzzle is stated as follows: There are some unconfirmed transactions. Choosing some of them, the miner (i.e.~the person/computer that tries to solve a puzzle) will form a putative block to be added to the blockchain. This @@ -437,7 +437,7 @@ picture shown in \eqref{unconfirmed}. If we don’t have such a linear ordering at any given moment then it may not be clear who owns which Bitcoins. Assume a miner David is lucky and -finds a suitable salt to confirm the transactions. Should he +finds a suitable salt to confirm some transactions. Should he celebrate? Not yet. Typically the blockchain will look as follows @@ -465,7 +465,7 @@ work on the longest fork? Well their incentive is to mine Bitcoins. If somebody else already solved a puzzle, then it makes more sense to work on a new puzzle and obtain the -Bitcoins for solving that puzzle, rather than wast efforts on +Bitcoins for solving that puzzle, rather than waste efforts on a fork that is shorter and therefore less likely to be ``accepted''. Note that whoever solved a puzzle on the ``loosing'' fork will actually not get any Bitcoins as reward. @@ -505,14 +505,14 @@ rest of the world avoids the ploy of double spend. In order to raise the bar for Alice even further, merchants -accepting Bitcoin use the following rule of thumb: A +accepting Bitcoins use the following rule of thumb: A transaction is ``confirmed'' if \begin{itemize} \item[(1)] it is part of a block in the longest fork, and \item[(2)] at least 5 blocks follow it in the longest fork. In - this case we say that the transaction has ``6 - confirmations''. + this case we say that the transaction has 6 + confirmations. \end{itemize} \noindent A simple calculation shows that this amount of @@ -522,23 +522,26 @@ can have their transactions been rolled-back for 6 months or so. The point however is that the odds for Alice being able to cheat are very low, unless she can muster more than 50\% of -the world Bitcoin mining capacity. +the world Bitcoin mining capacity. In this case she could +out-race the rest of the world. The point is however that +amassing such an amount of computing power is practically +impossible for a single person or even a moderately large +group. Connected with the 6-confirmation rule is an interesting -phenomenon. On average, it would take several years for a -typical computer to solve a proof-of-work puzzle, so an -individual’s chance of ever solving one before the rest of the -world, which typically takes only 10 minutes, is negligibly -low. Therefore many people join groups called \emph{mining -pools} that collectively work to solve blocks, and distribute -rewards based on work contributed. These mining pools act -somewhat like lottery pools among co-workers, except that some -of these pools are quite large, and comprise more than 20\% of -all the computers in the network. It is said that BTC, a large -mining pool, has limited its members to not solve more than 6 -blocks in a row. Otherwise this would undermine the trust in -Bitcoins, which is also not in the interest of BTC, I guess. -Some statistics on mining pools can be seen at +phenomenon. On average, it would take several years for a typical +computer to solve a proof-of-work puzzle, so an individual’s chance of +ever solving one before the rest of the world, which typically takes +only 10 minutes, is negligibly low. Therefore many people join groups +called \emph{mining pools} that collectively work to solve blocks, and +distribute rewards based on work contributed. These mining pools act +somewhat like lottery pools among co-workers, except that some of +these pools are quite large, and comprise more than 20\% of all the +computers in the network. It is said that BTC, a large mining pool, +has limited its number of members in order to not solve more than 6 +blocks in a row. Otherwise this would undermine the trust in Bitcoins, +which is also not in the interest of BTC, I guess. Some statistics on +mining pools can be seen at \begin{center} \url{https://blockchain.info/pools} @@ -546,26 +549,25 @@ \subsubsection*{Bitcoins for Real} -Let us now turn to the nitty gritty details. As a user you -need to generate and store a public-private key pair. The -public key you need to advertise in order to receive payments -(transactions). The private key needs to be securely stored. +Let us now turn to the nitty gritty details. As a participant in the +Bitcoin networ you need to generate and store a public-private key +pair. The public key you need to advertise in order to receive +payments (transactions). The private key needs to be securely stored. For this there seem to be three possibilities \begin{itemize} \item an electronic wallet on your computer -\item a cloud-based storage (offered by some Bitcoin service) +\item a cloud-based storage (offered by some Bitcoin services) \item paper-based \end{itemize} -\noindent The first two options of course offer convenience -for making and receiving transactions. But given the nature of -the private key and how much security relies on them (recall -if somebody gets hold of it, your Bitcoins are quickly lost -forever) I would opt for the third option for anything except -for trivial amounts of Bitcoins. As we have seen securing a -computer system that it can withstand a breakin is still very -much an unsolved problem. +\noindent The first two options of course offer convenience for making +and receiving transactions. But given the nature of the private keys +and how much security relies on them (recall if somebody gets hold of +it, your Bitcoins are quickly lost forever) I would opt for the third +option for anything except for trivial amounts of Bitcoins. As we have +seen earlier in the course, securing a computer system that it can +withstand a breakin is still very much an unsolved problem. An interesting fact with Bitcoin keys is that there is no check for duplicate addresses. This means when generating a @@ -577,11 +579,11 @@ The absence of such a check is easily explained: How would one do this in a distributed system? The answer you can't. It is possible to do some sanity check of addresses that are already -used in the black chain, but this is not a fail-proof method. +used in the blockchain, but this is not a fail-proof method. One really has to trust on the enormity of the $2^{160}$ -number. +space for addresses. -Let us now look at the data that is stored in an transaction +Let us now look at the concrete data that is stored in an transaction message: \lstinputlisting[language=Scala]{../slides/msg} @@ -637,8 +639,12 @@ \url{http://bitcoinmagazine.com/13774/government-bans-professor-mining-bitcoin-supercomputer/} \end{center} +\noindent +Bitcoin mining nowadays is only competitive, or profitable, +if you get the energy for free, or use special purpose +computing devices. -\subsubsection*{Anonymity and Government Meddling} +\subsubsection*{Anonymity with Bitcoins} One question one often hears is how anonymous is it actually to pay with Bitcoins? Paying with paper money used to be a @@ -670,24 +676,40 @@ \end{quote} \noindent The only thing I can add is that with Bitcoins we -will have even more fun hearing confessions like the infamous +will in the future have even more fun hearing confessions from +famous or not-so famous people like the infamous ``I did not inhale''.\footnote{\url{www.youtube.com/watch?v=Bktd_Pi4YJw}} The whole point of the blockchain is that it public and will always be. -There are some precautions that are suggested, like to use a -new public-private key pair for every new transaction, and to -access Bitcoin only through the Tor network. But the -transactions in Bitcoins are designed such that they allow one -to combine incoming transactions. In such cases we know they -must have been made by the single person who new the -corresponding private keys. So using different public-private -keys for each transaction might not actually make the -de-anonymisation task much harder. And the point about -de-ano\-nymising `anonymous' social networks is that the -information is embedded into the structure of the transition -graph. And this cannot be erased with Bitcoins. +There are some precautions one can take for ensuring anonymity, like +to use a new public-private key pair for every new transaction, and to +access Bitcoin only through the Tor network. But the transactions in +Bitcoins are designed such that they allow one to combine incoming +transactions. In such cases we know they must have been made by the +single person who knew the corresponding private keys. So using +different public-private keys for each transaction might not actually +make the de-anonymisation task much harder. And the point about +de-ano\-nymising `anonymous' social networks is that the information +is embedded into the structure of the transition graph. And this +cannot be erased with Bitcoins. + +One paper that has fun with spotting transactions to Silk Road (2.0) +and to Wikileaks is + +\begin{center} +\url{http://people.csail.mit.edu/spillai/data/papers/bitcoin-transaction-graph-analysis.pdf} +\end{center} + +\noindent +A paper that gathers some statistical data about the blockchain is + +\begin{center} +\url{https://eprint.iacr.org/2012/584.pdf} +\end{center} + +\subsubsection*{Government Meddling} Finally, what are the options for a typical western government to meddle with Bitcoins? This is of course one feature the @@ -705,7 +727,7 @@ blacklist Bitcoins (for example at Bitcoin exchanges). This would impinge on what is called \emph{fungibility} of Bitcoins and make them much less attractive to - baddies. Suddenly their hard-earned Bitcoin money cannot + baddies. Suddenly their ``hard-earned'' Bitcoin money cannot be spent anymore.The attraction of this option is that this blacklisting can be easily done ``whole-sale'' and therefore be really be an attractive target for @@ -729,7 +751,7 @@ \end{center} this would not be such a high bar to jump over. Remember - it ``only'' takes to temporarily be in control of 50\%+ + it ``only'' takes to be temporarily in control of 50\%+ of the mining capacity in order to undermine the trust in the system. Given sophisticated stories like Stuxnet (where we still not know the precise details) maybe even @@ -755,14 +777,14 @@ 2.0 will honour the Bitcoins from Version 1.0? \end{itemize} -\noindent Finally, a government would potentially not really +\noindent A government would potentially not really need to follow up with such threads. Just the rumour that it would, could be enough to get the Bitcoin-house-of-cards to tumble. Some governments have already such an ``impressive'' trackrecord in this area, such a thread would be entirely credible. Because of all this, I would not have too much hope -that Bitcoins are free from government \& Co interference when -it will stand in its way, despite what everybody else is +that Bitcoins are free from interference by government \& Co when +it will stand in their way, despite what everybody else is saying. To sum up, the technical details behind Bitcoins are simply cool. But still the entire Bitcoin ecosystem is in my humble opinion rather fragile. @@ -782,7 +804,7 @@ for example, solve protein folding puzzles?\footnote{\url{http://en.wikipedia.org/wiki/Protein_folding}} For this there are projects like -Folding@home\footnote{\url{http://folding.stanford.edu}}. +Folding@home.\footnote{\url{http://folding.stanford.edu}} This might help with curing diseases such as Alzheimer or diabetes. The same point is made in the article diff -r 7f0ac1355f0b -r 5a6e8b7d20f7 handouts/ho09.tex --- a/handouts/ho09.tex Fri Dec 05 01:17:31 2014 +0000 +++ b/handouts/ho09.tex Mon Dec 08 07:14:28 2014 +0000 @@ -1,6 +1,9 @@ \documentclass{article} \usepackage{../style} \usepackage{../langs} +\usepackage{../graphics} +\usepackage{../grammar} +\usepackage{multicol} \begin{document} @@ -8,32 +11,111 @@ If we want to improve the safety and security of our programs, we need a more principled approach to programming. Testing is -good, but as Dijkstra famously said: ``Testing can only show -the presence of bugs, not their absence''. While such a more -principled approach has been the subject of intense study for -a long time, only in the past few years some impressive -results have been achieved. One is the complete formalisation -and (mathematical) verification of a microkernel operating -system called seL4. +good, but as Dijkstra famously said: + +\begin{quote}\it +``Program testing can be a very effective way to show the +\underline{\smash{presence}} of bugs, but it is hopelessly +inadequate for showing their \underline{\smash{absence}}.'' +\end{quote} + +\noindent While such a more principled approach has been the +subject of intense study for a long, long time, only in the +past few years some impressive results have been achieved. One +is the complete formalisation and (mathematical) verification +of a microkernel operating system called seL4. \begin{center} \url{http://sel4.systems} \end{center} -\noindent In 2011, this work was included in the MIT -Technology Review in the annual list of the world’s ten most -important emerging +\noindent This work was in 2011 included in the MIT Technology +Review in the annual list of the world’s ten most important +emerging technologies.\footnote{\url{http://www2.technologyreview.com/tr10/?year=2011}} While this work is impressive, its technical details are too -enormous for explanation here. Therefore let us look at +enormous for an explanation here. Therefore let us look at something much simpler, namely finding out properties about programs using \emph{static analysis}. -Static analysis is one technique that checks properties -of a program without actually running the program. This -should raise alarm bells---the reason that almost all -interesting properties about programs are equivalent to -the halting problem, which we know is undecidable. +Static analysis is one technique that checks properties of a +program without actually running the program. This should +raise alarm bells with you---because almost all interesting +properties about programs are equivalent to the halting +problem, which we know is undecidable. For example estimating +the memory consumption of programs is in general undecidable, +just like the halting problem. Static analysis circumvents +this undecidability-problem by essentially allowing answers +\emph{yes} and \emph{no}, but also \emph{don't know}. With +this ``trick'' even the halting problem becomes +decidable\ldots{}for example we could always say \emph{don't +know}. Of course this would be silly. The point is that we +should be striving for a method that answers as often as +possible \emph{yes} or \emph{no}---just in cases when it is +too difficult we fall back on the \emph{don't-know}-answer. +This might sound all like abstract nonsense. Therefore let us +look at a concrete example. + + +\subsubsection*{A Simple, Idealised Programming Language} + +Our starting point is a small, idealised programming language. +This language contains variables holding integers. We want to +find out what the sign of these integers will be when the +program runs. This seems like a very simple problem, but it +will turn out even such a simple analysis is in general +undecidable, just like Turing's halting problem. Is it an +interesting problem? Well, yes---if a compiler can find out +that for example a variable will never be negative and this +variable is used as an index for an array, then the compiler +does not need to generate code for an underflow-test. Remember +some languages are immune to buffer-overflow attacks because +they add bound checks everywhere. This could potentially +drastically speed up the generated code. + +Since we want to + +\begin{multicols}{2} +\begin{plstx}[rhs style=,one per line,left margin=9mm] : \meta{Exp} ::= \meta{Exp} \texttt{+} \meta{Exp} + | \meta{Exp} \texttt{*} \meta{Exp} + | \meta{Exp} \texttt{=} \meta{Exp} + | \meta{num} + | \meta{var}\\ +\end{plstx} +\columnbreak +\begin{plstx}[rhs style=,one per line] +: \meta{Stmt} ::= \meta{label} \texttt{:} + | \meta{var} \texttt{:=} \meta{Exp} + | \texttt{jmp?} \meta{Exp} \meta{label} + | \texttt{goto} \meta{label}\\ +: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\ +\end{plstx} +\end{multicols} + +\begin{lstlisting}[numbers=none, + language={},xleftmargin=10mm] + a := 1 + n := 5 +top: jmp? n = 0 done + a := a * n + n := n + -1 + goto top +done: +\end{lstlisting} + +\begin{lstlisting}[numbers=none, + language={},xleftmargin=10mm] + n := 6 + m1 := 0 + m2 := 1 +loop: jmp? n = 0 done + tmp := m2 + m2 := m1 + m2 + m1 := tmp + n := n + -1 + goto top +done: +\end{lstlisting} \bigskip diff -r 7f0ac1355f0b -r 5a6e8b7d20f7 slides/slides10.tex --- a/slides/slides10.tex Fri Dec 05 01:17:31 2014 +0000 +++ b/slides/slides10.tex Mon Dec 08 07:14:28 2014 +0000 @@ -657,6 +657,7 @@ \begin{itemize} \item model checking\medskip \item program logics (Hoare logics, separation logic)\medskip +\item proof-carrying code\medskip \item specifications / correctness proofs \end{itemize}