you'll miss that basically k is is a
project for writing down programming
languages in so it's a language building
language is what I tell people and so we
have built the languages C and Java and
JavaScript and we're working on C++ and
we have Python and we have a lot of
other big languages and also some
network semantics and stuff like that so
basically once you write down your
language in K you have both the formal
specification in terms of a human
readable document and you have a range
of tools essentially that you can use
for experimenting on both your language
design as well as for running programs
and things like that so you get a parser
out of it an interpreter you get a model
checker a deductive program verifier and
we're working on some some new exciting
tools as well I see three the EVM
semantics was already finished actually
it started as kind of a side project in
a class and then it someone approached
us and asked us to finish it and gave us
a convincing amount of money to do so
and the ic3 basically I just extended
that semantics to include some kind of
higher-level language constructs and EVM
so it was just a few days working on
that but basically I added things like
while loops and if statements and
assignment and local variables and
structured control flow to the EVM and
then just had a small compiler down to
EVM itself and I called that language
EVM crime the compiler is written all in
K it's about 250 lines of literate K
code so most of it's actually
documentation so it was fairly compact
and that just kind of speaks to how easy
it is to build new languages in K and
right now that project is being used to
so we're writing tests for EVM crime
essentially and then we're also
extending it to kind of our goal is
something like a Viper - - so that we
can
and very easily compiled VIPRE contracts
into this EVM crime or this Viper - -
thing and then the remainder of the
compilation can kind of be well
controlled and well understood and then
also out of that which you'll get is all
those tools for VIPRE contracts right
you'll get program verifier and a model
checker symbolic execution engine all
those tools immediately provide for
contracts as well and then hopefully
also EVM crime will serve as a nice
compilation target for other high-level
languages one of the other things we
were thinking about maybe doing was
targeting lll if people are familiar
with that there's another slightly
higher level language and then that
would kind of give us the benefits of
having all the lll tool chains available
to us but you know I mean we're open to
suggestions in terms of how people would
like to see that evolve and you know
we'll keep on working on it and building
more languages on top of EVM directly I
think that's cool yeah so my project was
writing secure smart contracts and we
had probably the biggest team at the
bootcamp I think there were like 10
people on it or something like that and
it was sort of meant to be a dual
purpose project both educational and
constructive for the community so how
many people here have heard of hack this
site anybody use tech this site okay a
few of you so I think a great way to
train people train solidity developers
and smart contract developers in the
ecosystem on how to write secure smart
contracts and had a right proper code
that lasts a long time is by actually
having them getting their hands dirty
and breaking other smart contracts so
the first thing we sort of did was we
got all of our ten people together in a
room and we had them write in the ERC 20
with no other instructions other than
that just sit down and write in the IRC
20 and then sort of me and a few other
people went through and audited their C
20s and pointed out to them all of the
ways in which we could possibly break
them after that we had them fix their
ERC 20s and go through the REO dating
process until they had correct D'Arcy
20s and then sort of the second half of
the project was to build out this
platform hack this contract so you can
access it at hack this contract I
and the way it works is there's five or
six example contracts on there that are
intentionally vulnerable you deploy them
on the rinkeby Testament all you have to
do is give it your link of the address
and then have at it try to hack the
contracts and see if you can actually
break these things so future work
directions there's a few features
missing from the site which you'll see
if you try to use it I still think it's
totally usable and fun today so adding
those in is obviously sort of priority
zero after that I'd like to add in all
of the wonderful submissions we had to
be underhanded solidity contract contest
which you guys heard about earlier today
in the main room as well as examples of
all the past tax so I would like new
solidity developers to sort of come in
and be able to reproduce the DAO hack
themselves and write that attack
contract and I think that by doing so
we're sort of educating people on how
you can write smart contracts
incorrectly
and indirectly getting them to write
smart contracts more correctly so I
think it's a super-fun approach and I
think you'll feel good if you log on and
try to break a few of these things cool
hey I'm Nate deploy on a project called
peace relay so first of all to start off
who here is sort of PTC relay all right
a couple people the general idea is that
there's a smart contract on the etherium
chain that imports block headers from
Bitcoin and once you have bought block
headers a Bitcoin in a smart contract
what you can do is you can provide
proofs of transaction inclusion in those
blocks to the etherion blockchain
so an interesting use case might be
something along the lines of oh you know
pay me money to my Bitcoin address and
if you do I'll give you ether in a
trustless manner and so this is pretty
much what we can do with this idea of
relay contracts like crossed crossed NBA
contracts so the project that we worked
on please relay essentially we're trying
to be that for any two EVM base chains
essentially relay contracts between two
EVM base chains over the course of
bootcamp we built out one of these and
we were actually the you know pretty big
stuff here the first ever people to move
Rob's tanea onto rinkeby right I know
huge and the idea is that you lock an
asset on one chain you can then provide
a proof to the other chain using this
piece real a contract that that asset
was locked and what it does is it
instantiates like you know
setbacks token ERC token that backs the
acid on the other chain you can move
that acid around in the second chain
however much you want and when you want
to eventually move back you can burn it
on this chain and then provide a proof
over here that you've actually burned it
you know other than that to cover a
couple other interesting applications so
I mean the immediate application is that
you know you can move like et C or any
other EPM you know back coin straight
like neo or so like Gollum I'm sorry neo
and killed him to interim and so that
you know all the B central I can this on
a thorium country you know between two
constants in this coin so another
application is that you know now you can
actually you know move private coins
right in in some private chain because
of the you know interim Enterprise
Alliance so many people are like during
private blockchain with their own right
so you can actually remove the asset in
the private sale to the public chain and
you know trade between this coin and
other yes each what it opens
the other interesting thing that you
could possibly do is you could imagine
kind of so the idea is like you know
with peace relay one EBM chain can
become aware of another EDM chain on the
other interesting thing that you might
be able to do is kind of point the piece
we like contract that at the chain that
it's actually on and that might not make
much sense but kind of the ideas we can
make the EVM more aware of what's
actually happening in the EVM so for
example as kind of a spin-off of this
project one thing that kind of came out
of the summer was essentially a gasps
Oracle and so kind of you can imagine
that like the AEM kind of becomes aware
of how much gas is actually being used
on the EVM the reason that's interesting
you know you can imagine like you know
if there's this much gas used if there's
more than 50% of gas used in the last
100 blocks extend the time lock on this
to eternal state channel time out
interesting things like that right now
peacefully is being maintained by two
different team the first team is
carbonyl group and that based and the
second one is I guess consensus in the
isolate project and from carbon dioxide
we are planning to release some
better version a piece relayed by the
enemies this month or early early next
month so please keep in touch any other
question for peace really alright so in
typical runner-up fashion I actually
prepared a presentation so let me just
run through that real quick so our
project was front-running Bank art it
was done by myself to see Qureshi Ivonne
Bugatti and Preeti Katz ready so so
quick so uh quick note so this research
so we did this at I see three and then
we published the research on October
10th at the same time we worked with the
banqueting before we actually published
to address the vulnerability and put out
some fix so that it wasn't so vulnerable
to this I just want to point out the
bank routine was cooperative and
analyzing attack pushing out of fix so
want to give props where it's dude it's
still in early space people mess up all
the time you know blockchain develop is
really hard so that was cool so what is
front-running funding is a term that
originated back in the stock market and
in the days when trades were executed on
paper so literally what would happen is
a broker would receive a large buy order
from a client and they might say this
out loud so other people could hear and
they would go walk over the desk to
perform the trade a malicious trader
would basically going on or see this is
going on and literally run in front of
them to put in a buy or sell ahead of
time to profit and sort of sandwich
their transaction in between now you can
do the same thing on the blockchain if a
miner or user sees an unconfirmed
transaction in the mempool that they can
profit from they can squeeze their own
transaction to come in front so
essentially you're profiting from a
beneficial reordering of the
transactions now as a miner this is
pretty easy because the the way that
mining essentially works is that you are
sort of the leader for a moment you get
to decide what goes in that block and so
you can reorder transactions however you
want if you manage to mine that block as
a user however you can actually
manipulate where you go in a block by
changing your gas price and most mining
clients will sort mine transactions by
the gas price so if you come in higher
than somebody else you'll come in before
somebody else in the serialized
execution so many blocks free market
protocols are vulnerable to miner
front-running but it doesn't seem to
really happen very much in practice that
we can observe plus miners can only
front-running blocks that they
themselves happen to mine right so
unless we're coordinating among a big
mining pool if I'm a malicious miner I
only get the front run and it happened
to mine a block which is very very rare
for any
minor however if your protocol can be
front-run by random users that's really
bad
does that means that any user who's
sitting on the blockchain looking for
transactions can run everything in front
run any transaction that they want to so
banker was known to be vulnerable to
minor front running as many marketplaces
are but we demonstrated that it was
vulnerable to user front-running meaning
any user on the network could front row
and Bank row transactions and make money
so how does Bank work for those of you
who are not familiar Bank is
basically an automated liquidity
provider using a smart contract it gives
you deterministic pricing by maintaining
a constant reserve ratio okay so long
story short if you buy the price goes up
if you sell the price goes down that's
that's the law of the land for Bank Corp
okay so what that means is that if I
know someone's gonna buy I know the
price is gonna go up great so the attack
is pretty simple you launch a guest node
and you write a little bit of Python
script to basically monitor the mem pool
and see what transactions are going in
the network if you can if you can tell
that the transaction is one that
qualifies as being worth front-running
which that's basically that's doing then
all you do is you increment your gas
price a little bit more than what they
paid so do you can see 1g way more than
them then you you launch the transaction
and if all goes well you should have run
around them so running simulations we
showed that over a two month period of
July and August with 100 each principle
you would have produced $35,000 in
return the front-running transaction on
the main assuming that you know that the
market or the people in the network
didn't react which is greater than 100
percent ROI over that period of time we
also showed that because Bank is a
protocol that can be used by many
different tokens the smaller the token
mark you have the higher your ROI would
be for front-running that market and so
if there were a large number of tokens
that were using Bank run at that time
you would have been able to make even
more and so we also front ran a single
transaction on the main net just to
prove that this was in fact doable which
we did we returned the Delta that we
made to the person who originally made
the transaction and then didn't run any
further so how can you mitigate this
kind of attack so this is kind of
endemic to blockchains but there are
several ways to try to mitigate it so
one thing you could do is force all buys
or sells to specify an acceptable price
range so you could say okay I'll I'll
make this transaction but only if the
price offered by the market maker is P
plus or minus some Epsilon otherwise
cancel the transaction if you do that
this can't be front run by them
the users because you're guaranteeing
yourself a certain price however this
leaks important metadata if someone
front-runs you and then your transaction
is canceled they kind of know let's say
you were gonna buy you know a million
bank right well okay maybe your
transaction canceled but they know
someone's trying to buy a million Bank
so you know that bank card is gonna go
up so if they buy a bunch of banco and
they know eventually you're planning to
buy they know that they can just wait
for your buyer to come in and then they
can sell so there's also significant
limits your throughput so if if lots of
transactions are happening on on bank or
then it's very hard to ascertain how
wide that epsilon should be so that your
transaction doesn't sort of get
cancelled and occu ously right so
otherwise you just have to accept some
margin of front-running that you're okay
with if that epsilon you know ideal
obviously if you're buying you're okay
with the price going down but you
wouldn't to go out so it's not a great
compromise but it is better than nothing
however what you can do is you can set a
maximum allowable gas price for the
contract so essentially what that does
is it puts an upper limit on what people
are allowed to pay to try to get in
front of line of each other right this
is nice because it can't be fronted by
users however it's still vulnerable to
minor front-running cuz minor can do -
can do whatever they want it's not it's
not really you know they're not beholden
to accepting these rules so it's also
vulnerable to transaction flooding by
malicious users but this is expensive
and difficult in practice and not really
something that people have seen so this
is a solution that bank or settle on
it's a decent compromise between you and
security everything so happens in one
transaction just a few extra parameters
you have to send out now the ideal
solution would be some form of commit
reveal so in a commit reveal these are
well known for voting schemes in a
commit reveal you first commit to the
trans actually going to make by sending
a hash of the transaction plus some
nonce then you reveal the transaction
announced in a subsequent block
unfortunately for a commit reveal to
work it has to span multiple blocks to
actually make a trade so this is kind of
undesirable right like you know in
Spanish two blocks things can change
it's just kind of a slow crappy UX but
this is the safest scheme now doing this
naively is still vulnerable to certain
attacks so Submarine sense was actually
worked on by lawrence Breitenbach phil
diane ora jewels and florian tremor but
were they proposed a scheme for
accomplishing this securely
which is which is a lot easier with the
create to opcode which is offered by EAP
86 which is not gonna come out in
metropolis unfortunately so we're still
waiting on that we're also exploring
other practical commits reveal schemes
that are possible with
with current op codes so that is front
running there was me me prithi Ivonne
social thanks to re Jules Ito been
Tawfik Karl flourish for helping us the
research and of course to ic3 Thanks
[Applause]
thanks guys
[Music]