[Applause]
as everyone for coming who have now a
workshop on the form of replication of
smart contracts and maybe before even
typical of topic so how many people have
done any for modification of contract so
far maybe this raise the hands so very
few so I guess all the remaining ones
will attract it by the last part that's
supposed to be easy and hopefully by the
end of this workshop everybody manages
to have a hands-on depends on exercise
and everybody should be able to verify
some form of properties on contracts so
the people who peed in the workshop we
have Demeter there his previous student
it is during a joining chain security
now parents demand for modification and
problem analysis then we have also
hunter permanent so he is the lead
developer of the very far we'll be using
today in the workshop and also who were
visiting back there city of chain
security and myself as well so who we
are we are a chain security we are a
spinoff from ETH Zurich ETH the
University not the foundation based in
Zurich Switzerland and we focus on the
objects activity we have worked with
many blockchain projects so far we can
them over 80 audits not only smart
contract always but also product of all
its platform on itself as far as a cup
of very visible ie IDs I think many
people are recognized the chain security
name from you know some of those
earpieces we have reviewed in the past
and so yeah we also have quite a few
already security products with platforms
at the CTO Foundation polkadots
silica and fewer than some chains where
we focus on building security tools you
know tools for finding boxes no enfant
as far as for modification tools for for
these platforms all right so it's part
to the work we have done quite a couple
of systems so far so I have listed some
of those
some of them on this light here and so
this is the name to achieve different
goals we typically combine techniques
from various different domains such as
tactical asset dynamic analysis we also
use quite a lot of fun everybody thinks
of machine learning to to you know to
build these systems so some of you are
familiar with the Sakura fight this was
the first system that were built back in
2017 it's a system for finding generic
on the abilities in smart contracts and
yeah so that's was basically addressing
all these puzzles were popping up
regularly every couple of weeks in 2017
in all these you know parity walnuts and
many other contracts so this is what
that system was addressing and so this
system along with other system I think
they made a difference in the sense of
2018 we will actually so much fewer
facts because of such generic like
really simple boxing contracts so
another system we have builds is with
every wedding system that addresses the
problem of ensuring functional
correctness so we're going to talk a
little bit more about what functional
corrective correctness actually means
and we have fuzzing system that
essentially generates transactions and
tries to find violations of the specific
security properties that we're trying to
to check for or for a small conference
and the main system that we will be
talking about today is the direct system
which is the first automated verify for
for verifying smart contracts this we
have a demo on variance of CH we have
some few other instances of this system
that's one
for the exercise later today and for
people that are interested really in
depth on how that system works what
guarantees it provides so we also have a
research paper which will appear at the
to Boise possible security and privacy
so that's one of the main security
conferences one of the main academic
security conferences so if you go on our
webpage chase younits.com I go to
research you can download the PDF and
read all the details about the
verification technique that is being
used in that system alright so before we
actually do I you know go into the
hands-on exercises it's important also
to mention why are we actually doing
this and the main reason is that I mean
where they initialize how many people
have verified contracts I think they
worked about two three hands and the
reason this is is that you know thermo
replication used to be this very
difficult time-consuming task or you
have to be really an expert in formal
verification have a PhD in logics and so
on to to to prove that a contract is
correct and if we are to make form of
ratification mainstream you know a lot
of developers also adopting that
approach then you have to be building a
system we have to be building systems
that allow people without this
background to write functional
specifications and prove the contracts
correct and that's exactly what this
very very very far aims to do so it
eliminates this nest needs to know
in-depth knowledge of form of
verification and takes down this reduces
also significantly
vacation time because I suppose it's
really not a very hard task to to verify
contracts with such systems so we said a
system if you take something like a
standard ear seat when it's open which
will look in-depth in the exercise you
can literally no formal ratification for
all the main properties you will care
about a token you know in a matter of a
couple of hours that we done with with
the ratification ever visit here some of
us some someone that we have verified we
have more on our main webpage a spirit
of calm / audits or you can find some of
some of these reports where we have done
proper verification of those all right
so the workshop will continue as follows
so we'll start with some very more
high-level introduction to what
functional correctness means and why is
it challenging to formally verified
properties with functional properties
and what are different techniques that
different tools are introduced in that
space what's called a different person
guarantees today so also will cover here
of course that the correct system and
then in the second half you'll switch to
a hands-on exercise where Demeter will
talk walk you through how do we specify
properties and verify them with with a
verifiable Eric's and so we've also
about many other people from the chain
security team back there so they will be
assisting you while doing this exercise
and then in the last part depending on
time we'll try to get into some more
detail about the actual verification
methods and how this is being automated
by the various verifier alright so let's
get started and functional correctness
so what is functional correctly so
usually when people think about security
tools they're these kind of tools where
you just paste the codes and then they
show you a bunch of on the business that
founds so this is not what we're talking
about here so we're not looking for more
dynamic movement
were talking about functional
correctness and what this means is that
whether the problem of functional
correctness has two parts so honest you
have this hard culture that you want to
prove that if you wanna you want to make
sure it's correct and then the second
piece of information that you need is
the functional specification of a smart
contract so a function specification is
that this is the thing that this defines
what is what is the intended correct
behavior of that smart contracts okay so
to make this a little bit more country's
here on the Left imagine you have a
smart contracts that typical year z22 so
you have all these terminals that
balances total supply order a couple of
functions that allow users to to
transact with the contracts and then the
functional specification typically
consists of requirements such as the
seventh caller balances equals the total
supply okay so don't even this
specification says that all the tokens
are assigned to users somehow there are
no missing tokens on the side to know
about the sign to end user another
common example is that often tokens are
immiscible meaning that you can increase
initial more tokens and often you wanna
show not only certain users can exercise
its functionality and if you want to
make sure that if the total supply
increases then that was triggered by a
transaction issued by the owner of the
contracts okay and then typically you
would have a huge list of those
requirements that you would have to you
would have to check that whatever the
implementation of these functions is it
is indirect with respect to these
functional requirements okay
so technically how does how do we
actually check that the the code is
correct and they're roughly speaking two
steps so the first step is well to
essentially transform this English
description of correct behavior into
something that's to take them down and
to specify them at the level of the
source code okay
so for instance if we take the first
requirement that says that the server
balances has to be
power supply then this is written in the
specification language that we'll be
using later and exercises of the very
excess specification language and this
is how it will look in the actual
specification language so fairly
intuitive they'll succeed some keywords
onto the mapping that we're trying to
sell and then we have a quality with the
focus of okay last that number one is
inevitable you know you have to be able
to transfer formally state what the
property means and once we have
formalize it then if we have a
particular state of the smart contracts
then we can check the whether this
property holds or not alright so for
instance if we look at a state where we
have two users having balanced 50h and
we have total supply one other than the
property holds with us that's what it
says and here would be an example where
the property down the hall because this
sum of these two balances actually
exceeds the total balance specified in
the contract et cetera so a step number
one define the property step number two
is to actually check that this property
holds for all possible states that your
contract could reach okay now what does
this again technically mean well once
you deploy the smart contracts on the
blockchain it is always initialized by
the deployment speed so it will end up
in being some specific initial space so
that's what these days and you would
have to make sure the property goes
there so for instance you deploy and for
that initial state the sum of balances
would have to be equal to the total
supply okay that's one thing the next
thing is that once deployed the users
could send consent a transaction to the
smart contracts and each transaction
would modify the state of the smart
contracts so they can for example with
submit a mean transaction with different
you know different policy s arguments
and so on and let's be a little bit more
precise what these arrows and boxes here
represents so what these boxes
represents is the actual state of the
contract and the are started
I'm triggered by the transactions
submitted by the users and how are how
is our disposition defined this is
defined by the implementation of the of
the functions in the contracts so for
example if we have here we start from a
state where total supplies of hundreds
we have an older user with address
extend and then we have two users with
balances 50 tokens each and then main
function is defined such that it would
increment the total supply by the number
of dollars water two means and then it
would assign the new totals to the to
the owner of the contract so here if we
have this means one fiblets tokens
issued by the user base bill the normal
supply will be incremented as defined by
the function and then the balance of the
owner who has addresses euro extent
would be incremented from 52 also number
because that's how many additional
conservation so that's what this allows
you me alright so here comes immediately
the first immediate challenge when you
talk about functional correctness is
that even if we want to consider whether
the property will hold after one single
transaction after the first transactions
entered a contract that already gives
you so many different ones actually to
put that would be the test to be
accounted for that it becomes infeasible
to put foresee it's not possible to
another these transactions into actually
check them in all these things the
property will always cause and challenge
number one and we cannot stop here
because after the first transaction is
the user would submit second and third
and so on transaction and in fact
there's not lots of predefined bounds on
how many transactions this contract
would process in his lifetime so
to consider number of transactions you
were to formally verify that this
property would always hold their two
fundamental Chinese heroes all right so
let's very quickly go over what are
different techniques that could be used
to address this problem of taking these
formal properties and how they different
types of guarantees and so I ordered a
based on reliability so starting from
least reliable going towards more more
reliable techniques
well the bottom we have the menu reviews
always the human can look at the codes
understand what it does and try to find
violations so this is a successive
penetration testing property try to try
to crack the contracts and the
disadvantage here fairly well and also
it's a time consuming problem even if
you have especially we have big
contracts that would take a while for
for the security expert to understand
exactly how these things how of the
functionality of the contract is then
let's move over to model 26 so next
level would be to do some form of
automated testing and then primarily in
general for software but also in the
space of contracts two techniques for
testing contract so one is based on
fuzzing and the second major technique
is to special support execution so let's
briefly see what this what what these
techniques would do to this problem of
objective functional practice and so
starting for fun with fuzzy here's
basically what's happening so fuzzing is
a testing technique or a puzzler would
generate random transactions and then it
will execute the transaction some of the
contracts and by doing so the buzzer
would observe different states of the
smart contracts all right and by doing
so we can for all the states that have
been observed after posting these
transactions that we generate we could
check whether the property is violated
or not if it happens as we reach a state
where you get a violation
then the father would also return that
sequence of transaction that triggered
the violation and the developer could
see you know reproduce the buck and try
to fix it there are many many fathers
have been deployed that are available
online to do exactly this this thing
the Challenger typical is how to
generate transactions in a smart way so
you get verified coverage over at least
a very high code coverage over the
contract which is already pretty
challenging in contracts which tend to
be very stateful and complex
preconditions of the transactions and so
on so what's funny was no idiot would
not give you this full guarantee that's
why it's a testing technique because in
every time there will be some states
that you would not not observe simply
because the puzzle did not generate that
specific sequence of transaction that
would transition the contract to the
states so it's a testing technique
essentially now symbolic execution
that's something different symbolic easy
techniques that it is based on this
symbolically special technique it simply
would not scale to reason about such
depth of transaction so typically if you
the symbolic symbolic to you would give
it as a mouse so it would run for maybe
thirty minutes one hour and then you
would stop and then it would reach
certain level so it is better at this
kind of breath exploration and but if
the bugs are hidden deeper like after
five ten transactions which could happen
even in simple contracts across cells
were you have to transition to example
two some refund face where you exercise
it on three week on functionality so
this typically tend to be somewhere
lower that are harder to explore with
similar tools so I have listed here some
other open tools that are available
that's
to do this okay it is clear so far if
there any questions just raise your hand
you can also go to this point itself all
right so that's the best thing and then
the highest level would be the formal
verification what this workshop would be
about and this is really the point where
you have a slip from testing to for
verification meaning that you could
actually prove this property for
whatever sequence of transactions we
would make it would always holds no
matter what okay
measure difficult happens at that point
all right now so let me show you what
this means is that you cover all
possible states essentially and if you
will check out of them and if you check
mark all of them you grab this for
guarantee right so that's what the
variant system does and you will be
losing its own and the input system is
as we solves the smart contracts as well
as the specification because we're
dealing with functional characters here
and the main thing of that what the
making of verax does is it it's fully
automate this process of fully optimize
the process of verifying in the sensors
it's if it's successful it verifies the
property it can down give guarantees a
is for it is fully verified and if it
fails to verify the property then it
doesn't give a guarantee whether the
property does well they're not so it
could be like you have to help a little
bit to actually verify the property or
it cook another property is valid and
then you have to pick the contracts so
we'll see some example so now
sighs later all right so to give you a
bit of something that we actually spent
quite some time is to ensure that verax
has a very intuitive and easy-to-use
facilitation language because that
typically is one of the bottleneck when
we talk about functional correctness is
again to use functional correctness in
addition to the contract you have to
write down what the contract is supposed
to do and if this is very hard and
tedious of specifying you you know you
will end up not not really using the
system so I will get a few examples of
specifications that we have seen to very
frequently appear in real world smart
contracts so this is something we just
observe doing audits and verifying
contracts and so this is a this is
literally what the specifications are so
you don't have to write some elaborate
scripts or something very complicated to
formally state of property so common
properties are things like access
control or you wanna ensure that certain
functions can be involved by particular
users is he saying that in always in the
contract if there was a transaction to
deposits then that was that transaction
was made by the owner of the contracts
another common party that we observe is
that very often it's not about who is
sending a transaction but it won't in
universe states the contract is so for
instance here we say that if the current
time exceeds the refund time by a week
and users are never no longer allowed to
submit refund transactions
yes state machine properties is as well
so again contracts are very stateful
there's explicit state variables that
define how the states how the contract
in addition to the different states so
you have to make sure that these
transitions are implemented correctly in
the contracts we saw an example earlier
I suppose so we have some over basically
aggregations over mappings in a race now
also tend to be pretty common so that's
we have at least explicit keywords in
the language to allow users to to run
these properties and another common
pattern is that so typically we have a
project it's not implement the full
production of our contractors in several
contracts and often there are certain
invariants that software dependencies
that are exists between the contracts
and their properties that's capture
these dependencies we have to verify
that they are implemented correctly in
the conference ok so again you will be
writing some of these so these
specification so a bit more technically
four he went the cinematics of the
specification level is actually based on
something on a fragment of that product
which is very well that it's a
specification language if you go back
take the case of research in this soit
is very well understood complexities and
expressivity and so on
alright so I want to depth on how how
the verifier actually works but in 30
bit combines two techniques one
technique is it does use this symbolic
execution technique which is very good
at handling dealing with many different
I contribute you submitting transactions
and then to deal with the unfounded
depth that users will
use something called predictive
abstraction that allows it to fully
capture all the possible that is very
large unbounded three to capture it with
some finite representation so the plane
equal time we may get you know it's more
details about that disease
alright so that's what the fellow intro
and now we're going to transition into
the actual exercise on how to use
vericsson to specify these properties so
hand over to me to introduce an example
uses yes okay amico yes and now we can
here with a small exercise to use
Ebonics by the way if you have any
questions at any time this raise your
hand and we can ask the questions the
goal here is to make the exercise more
inter and not so careful okay so so the
first step in proper verification is to
actually specify the properties
informally this means that we specified
any natural language whether it's
English or some other language you just
need to have some clarity over what's
this smart contrapposto right and in
this exercise we'll look at two main
confidence
what is your C 20 okay the other is kind
of standard ground zero of course
simplified because we don't have too
much time
okay so first we'll go over specifying
functional requirements informal right
and we we go this is fragmented of your
C 20 interface for those who are not so
familiar with the contract si si
dimensions one is total supply how many
tokens are in circulation
the average gamma so you can put in how
much tokens given others or accountants
and the
actual main function here is the
transfer function with well descended of
the transaction right can transfer some
tokens from its own account to the
recipient so we have the other service
recipients account and self amount
affected or any tokens sorry not that
these tokens add water
that's right and now whenever we are
specifying behavior of contracts we do
it over the contract and not over the
interface so here at the relevant parts
of the actual contract right so the
functions we have the balance the total
supply and Varmus become fields in the
copy right so these are not private
field search total supply l mapping
which says for every other issue account
how many tokens these others possesses
right so this one is new and which is
among others right and here we have some
specification pension transfer now when
we're thinking about the context of this
specifying its its brightness me at
least as abrasive belt when I am doing
this piece I never looked it into the
implementation right so for me the
contact is a black box and that's why I
specifically omitted the body of the
transformation hey Cheryl ago is to just
come up with a couple of properties
hopefully food center properties that
specified the core behavior of people
okay good so let's do this a little bit
more interactive
first properties on me right so we
already saw in our tree it says GC
formally in English of course my always
equals simple powers right so these pans
services specifies an invariance will
invent me that the holds of all states
and we are content something that you
like the false you know we need to
specify
invariance about the transfer function
right so suppose suppose when you start
a transaction with a given transfer
function you have a specific recipient a
specific amount and what will be the
usual case of so I will move like yes so
I would say the amount under of the
sender needs decrease the amount of the
recipients needs increased by the amount
the balance of the recipient needs
increased amount and the total supply is
not allowed to trade the total supply is
not allowed to change yes you're right
yes
so this is very good requirement we can
elaborate a little bit more so just to
repeat right you decrease the sender's
accounts by the given amount you
increase the recipients account when you
give on the mouth and total supply it
should remain the same right but one
thing for example of abilities so we
said the total supply should be the same
with these transfer could have
transferred tokens from another account
right so we didn't specify this so what
we get is a partial specification right
so in addition to that we need to
specify that all other accounts remain
unchanged
it's now is the total supply and as a
consequence the totals of 1 will also
remain unchanged
okay okay so we also do this in the case
the sentence you can't raise sufficient
funds right sufficient amount of tokens
if it doesn't have the function should
not do anything right so the first case
a little bit more elaborately right if
the message center is not equal to be
recipient right otherwise you don't have
anything to do and there is sufficient
amount of tokens in the balance of the
message sender then the most eccentric
account the balance should be decreased
about the balance of the recipient
should be increased by the new amount
and all remaining balances should remain
unchanged this is kind of a fairly
straightforward in formal specification
so what will be the remaining days so we
have one more kids
balances yes yes you're correct number
of boxes should be the same as the other
specie spent implicitly assumed so if we
go back a little
this is kind of implicitly assumes we
have this mapping it is kind of
continuous containing account for
everybody every possible address in the
world
it's very large amount of all possible
addresses it will help the idiom kind of
fragmented Sarika language takes care of
this is exactly yes
so what we do is we consider the
alternative things right so weak at
least deep in alternative is the logic
indicates the conditionally which means
that intimacy center is the recipients
or the powers are not sufficient right
all balances should remain and modified
right
yes overflow at this point
I'm not taking into account overflow at
this unit yes you are absolutely right
so when you're doing specification is
very easy to miss um well also the same
way as your problems nothing for example
here it could happen that these
conditions here are satisfied when over
hopeful happens because we have modular
arithmetic here within a volume with
addition and subtraction everything
works fine even if you overfall
something and the bronies will not work
or something the actual amount is not
the only it's generally not the
gorgeousness attack so in this example I
don't take into account so what you can
do with verax is depending on your
property you can specify the situate
that it will automatically fail to
verify the overall Stefan right but what
we currently do it very easily
we don't explicitly check for goals but
you need to write your property situated
okay and the other thing is you can
think of the specification then formula
was referring to actual integers where
there is no overall tonight this is
energies the informal that when you go
to actual formal verification you cannot
think means this way right okay so this
is your formal requirements for ESD
point okay now let's go through with
something slightly more elaborate we
have a constable
and the girls help is the bow feels so
accountant self conflict the multiple
enter which is raised the goal at which
you want great and because in faculty
culture and behaviour of the conflict is
that whenever somebody sends money to
the invest right this is a parable
function the console control deposit is
ready into the escrow right and it's
when somebody walks close and it's about
time to get close right after the tall
stack has passed and the many countries
we have two options either the goal was
raised in which case the beneficiary of
the tunnel cell and we drove the money
from the escrow or the goal was not
produced in which case the investors can
play different for the actor which will
be said and this logic should be
realized in the tester ownership so here
what we do that is marketed deposits our
money how much I turn each other is
deposited into escrow and to beneficiary
who in case of success will receive all
the way so on let's let's try to specify
this again important right so
again let's do the placement so the goal
and call time always remain the same
right so so this might look like a
stupid in formal requirements but in
incivility these things can change like
the skills of your contract decent stuff
in storage potentially they can change
so because of this we need to be
explicit about which things do remain
constant or shapes can change that
services a requirement that is all all
optimists and people other suggestions
right so just to implement the logic
that we informally is tied now in the
informal language no need to be very
sensitive
sorry close some we will only work in
the past the first time those who only
work if you ask because yes so what does
this mean
because we only work if it was to close
them sorry now first time
well if not with less than clothesline
call the co-sponsor
must be done successful yes yes so you
can specify that this this is one option
oh let me see what's the like nice
property I specify here is because yes
but maybe maybe it's something along the
lines of close so what does it say soon
if you know it's it's something else
right itself so here just for the sake
of the workshop I have the properties
fixed so welcome to say any proper cases
I will add them to the slides images
work with something says the properties
and property B here's a similar investor
proposes equals the vector in escrow
unless to be successful so this means
that you can also grow or change money
from SPSS okay so let's see sound
something more escrow never allow the
pot with drawing and painting the
movements I said this was one of the
requirements we
and more yes investors cannot claim
refunds after council goal is reached
and thank you you can figure out what
would be the complement to this no
problem and the complementary for the
next property needed to talk about this
this behavior gets beneficiary can
withdraw after cross so beneficiary can
only withdraw off the cross cell voltage
yes beneficiary can only withdraw a nice
color could tell sahabis reach you can
say something in many ways stone yes but
it's the same so when efficient cannot
be dropped before L cell voltage so we
have these I now this is most likely in
complete specification the behavior of
the calcium so providing the full
complete specification is a difficult
exercise and whenever you have defined
your context you don't need to do it
depends but this means you should always
keep in mind the facilitator finished
some news so now we have a bunch of
properties and what we can do is we can
just attempt to formalize them and
specify them in the barracks
specification language and try to verify
ok any questions
one question is as you're going through
the requirements is you saw that if you
go back to the specific interface for
the contract
the crowds tale there are three states
open his success and refund yes but
there's there another state where you've
reached the goal it's closed but the
beneficiary hasn't gotten around to
claiming the thing so it's kind of
ending is my my question is with regard
to the interaction between this code and
the specification you go back to fourth
and change the this code based on your
understanding of the specification so we
feel we can develop the content together
with the specification yes this is going
it's going to the you you look like and
for a variety of the requirements you
see that to be something you will change
the codes and maybe on the other cats
you did some in the specification which
is wrong and recovery price it correctly
interchange the specification it's so
this process you can be shown
cuz it seems like here there would be
some kind of limbo state where there
will be a ballistic
yes opportunity there'll be any with
states was the girl's back is an inch
and these girls matter who is not to
call this right the escrow will still be
in an open state and you cannot do
anything basically you disciplining the
state's suspending the beneficiary never
gets around every day
you've got paper eyes and that's you
know so it remains a little stay forever
show okay so then you need to make a
requirement you can expect a little
spent in make the next requirement as I
said specification waste is incomplete
so there is something else ready to go
shows what it said you can escape the
the you know state this is total -
property rights cannot verify -
probabilities they different techniques
and what we focus on properties of these
kinds which are called safety both of
these yes but yes does this kind of
reverse should we have the formal
requirement perfect
depends on your style thought hell
develop the codes and so some people
refer to an idea called so they
understand the program you might benefit
and then you go the specification some
people try to develop the specification
before they understand it and also if
you're providing an audit service you're
not writing the code you're you're hired
through yes delight respect exactly this
is sure what people eat a snake
yesterday they don't taste the cold or
they do suggestions in public illusion
was in general yes we do like the
specifications sometimes based on the
clothes sometimes based on requirements
given by the plans yes what about
investment in list yes
after the
whether you can invest after the goal is
arranged it should not be possible you
should not be possible to invest once
yes yes absolutely I said the
specification is right so ideally we'll
get the complete specification but
theses and of open-ended sources require
something okay so this one the whole
point of this is to emphasize that
before you start with formal
specification it's good to have informal
good sure okay let's move on my findings
with Erics
we try to formalize these properties in
the specification languages by sports
I see whether they verify okay so how
things get into the specification
language and the product is based on
something called the linear temporal
order so this might sound something very
natural so it in fact it is a brief
explanation so many most of you are
familiar with classical loading which is
our everyday logic that we use and you
can express formalized properties for
example the H is lose the nature for TCU
right so classical logic defies the
relations between individuals in this
case revelation is that the zoom over
two inches is even right and how would
you write this formally in plastic
project you say there exists some
integer sisters antibodies who is the
ancient ball is wisely seen together
Thank You snow you say the things are
even this is fast apology
and therefore logic adds a lot of
dimension to this which is titled right
so now these are not a statically laid
out in the perfect ideal world but we
also have promise and temporal body
forces could be violations in most
states so you have usually initial state
in nineteen point zero point one another
state and so on is itself now you can
define the relation and here we just as
an examples that you'll make accessible
and so is the case the ATO bodies which
is the danger is even so we've just
changed to property very slightly by
adding the movies and pepper
operator to express this this relation
which is an across time not just within
a single state right so you see that
this this this relation is not in the
real world right is he always the same
pages or even somebody the same
increment H one guy income as night the
same will become all right so this is an
example
property result because it's not always
the case
so yes that is what this is you and me -
yes
okay so just to say what you are
specified with the temporal logic what
you do have is this model panel you
specify properties of places for me and
each place is the sequence of space
right the index of the sequence gives
you can discrete time some time
progresses from 0 to infinity going in
increments of 1 right so for example
this could be the desert state or some
people might like to come from one
because respect and this is the second
step this is interesting
so this is kind of what your specified
in temporal logic and each state we have
randomly divided two worlds or two parts
that are the constants in servicemen's
and the variables of slightly and as an
example Alice as a person is a constant
which means that if this object does not
change across time policy advice is in
all time points right the same goes with
reverse osmosis and 27 rotate so this
insert constant they never change the
cross and the other part in the state
variables this is our position so
variables can change this piece is
really kind of water state contains
contains personal right
and on when we write a formula like
walking group itself statement amongst
time it is good tool to say what the
mental model is and how you liberate
those things so here is the different
example we have temperature right so we
have States and our state the base
constant and the variable is the
temperature in this paper so time could
be days in this case so we did not
specify in what units the time its
measured its out the screen I think
water spicy food the penalty see is this
property here which says in virtually
always real antigen is at least 11
degrees right so it has some property
and you don't to see whether this is
true for these things so this is the
thanks I need to see whether this is
true what we do we start evaluating the
the truth of the still ordinance of the
parts of the sentence across the states
and for example that we kind of the
innermost part is technicalities at
least 11 degrees right so how would you
see which states this statement is true
within each statement we are kind of
almost like classical logic to the movie
right and here we can see the
temperature is on degrees in the first
state in the Penn State and the last two
states here so time can continue opera
assume the temperature remains at least
11 degrees or so this is where this part
of our statement posted now you don't
see in which states the always at least
11 degrees holds true we need to look at
the same formula and see whether it
always
right so always means it may be but
after four this is passport right so we
can ask the question is it always the
case the temperature is at least 11
degrees in the initial state is all true
because in the subsequent state the
temperature is 10 degrees it's no longer
at least 11 right so it's not always the
case that the temperature is the place
to learn degrees in the initial spin
it's also not always the case that it's
in all these states until the
temperature stabilizes or let's say goes
below 11 degrees for n so from these
points onwards this part of the formula
will evaluates to true
right so let's be straight so is the
case with temperatures based learned
agrees and out the final careful
temporal operator the root canal to hear
is eventually the case is always
temperatures these 11 degrees and
eventually is true in a given space in
the reason future state when the soup
sentence your Navarre is so in which
space is the full sentence
and so it is yes everything everything
yes because no matter which state I
evaluate this this formula here there is
always a future state where it's always
the case that the temperature is at
least 11 degrees and this yellow light
dungeon in which space honest it's all
these I guess I don't understand the
meaning of that future state because how
do you know it's turn up because there's
the heat death of the universe that's
where the temperature will not be so -
so this is just an example it's an
example but there is no that is not
saying that we don't know there's going
to be a deep death or not so okay okay
you're absolutely correct
so for these sentences shows we cannot
require it but the wording liveness
property spherification form of is need
is more questions okay good so let's do
a small quiz register receipt of this
temporal logic queries right and if you
this is very unfortunate because this
should be a circle
so we have two squares which is very
important
it's all printable character yes he has
response Donuts anyway both oh it's the
walls right so we use the small square
to say always how do you say the diamond
to say eventually and the Botsford is
next something is doing the next step so
what does this sentence say right you
have two formulas or two predicates P
and Q and this thing says be advised
that eventually to write these purposes
so of how do you interpret this
informally with what we understand
okay let me tell you either there's pee
there will eventually here will happen
yes there's pee yes soul soul yes I put
this example just to represent something
when we are a volunteer for dinner will
ever I think it's always in the initial
state right so there is a slight
something in this sub script written by
we're always about the initiative site
so you're almost yes right we operate
these militia say if initially P is true
then you start with your moment or the
current moment eventually song is for
the current moment coupons and what you
said we can formalize with it's always
the case he holds eventually so no
matter whether its initial state or
initial state for every state in this
boat okay so what about this one always
eventually they just get some
alternative description of this
yes it's a possible 4p never happened
yes you can play with the de Morgan's
laws yes yes this is alternative
descriptions but it's another game with
alone this is purely off exactly yes so
you can interpret this because we have
to have time for anything theory you say
P is 2 infinitely offer me it's always
the case eventually P holds but if we
eventually result in some futures that
it also must eventually also this will
be different right and what about this
one
if we swap
venturing always because yes okay I just
wanted some floral oh that is $50 off a
shelf a face spell on what is written in
these little oddities this basically
says it eventually be stabilizes and
from certain moment onwards P will
always be okay well we have Sigma show
so we got into this one so what does it
say it's from any state that is produced
through that state every state over in
every state after and why is these days
this is this is this is the boss next
but it's true
actually what you said right so if you
interpret this next as next right
it's always the case right if P holds
that in the next case parents never P
sorry P will never be true why do you
know
then the next state would be Q and they
are not mutually exclusive
I'm officially exclusive then also that
I just fear is always followed by yes P
is always followed by the decisions
right and now you have what you said
right is if P holds afterwards all words
and to infinity Q will pop good socially
sure most of us one of us we put so many
buddy okay so this one is more complex
it says it's always the case there is
some constant and signals in this case
the block equals them and in the next
case
rocky possible possible yes the closest
value and yes the clock always
increments by 1 this is decision all
these property steps and assorted
so this is kind of food temporal logic
right you can write many complex
formulas and statements in temporal
logic code always ticks ticks by one
increment is correct yes
around three four four four four is down
the dog it doesn't move okay it's okay
good so now how all these applies to
smart companies right so what we do here
we need to fix you up kinda needs first
first and foremost and what we do is we
do the following we have world space in
the world states are the states of the
whole ball chain in between samples
right so whatever you're gonna depend
somewhat change to always around the
thing inside the transaction and our
space will be the boots length of the
book chain and diamond comment means the
execution of a single transaction right
this is what we do and we don't support
the food that parolee we serve on Jesse
primarily which is called canonical
safety bragging but are not gone in
details and roughly looks like this
he always your formula soup of this form
always P will be some formula of the
point shape so you have logical
conjunctions p.m. you have distinction
people it has implication P implies you
have this very interesting operator
which is temporal operator one speed
which means that once in the past it was
called this is the primary person of the
eventual operator so we can eventually
meaning in future moment P will call
this reason in the past few scope or the
current speed yes who is one
who are these ones of those swans
so it's not exactly wants me that these
ones so II some possible this is what we
do
and finally whenever you have some
expression you can refer to the previous
value of this expression so this is
similar to the next operator so in the
previous states the weight of this
expression was something right so nearly
one refers to the previous value of the
expression piece of the pie spins by the
way what happens in the initial
statement there is no previous thing
what do you think so when there was no
initial stages for simplicity we take
the previous method with equipment in
the usual state remember it is very
sometimes okay and now we have some
specific because we after all drinking
some video so all these we support suma
topics right so universities among a few
second token contract we can refer to
the same of all these things function
reduce the the name of the function
which is called in this transaction the
top level function feminised of course
we kind of start business that goes away
we can refer only to the top level
transaction the transaction we can refer
to function rights so this is the syntax
for defining the function name we can
also affect the balance of functions so
since this is a little bit emphasized we
are going to be moving in the future so
this is the zeroth argument the title
information and if you know what you do
is you know
canonical name of the function so this
is the name of the counterplay of the
function and here for the signature of
the function with addresses and this is
what Evers yes okay
so we don't support specification of
love invariance so all we do with spaces
specified let's go a transaction in
readiness starting our thoughts across
transactions what if we have known
Toulouse in the country it's shown in
some cases we can rewrite us rewrite
them without whose but if you have not
develops we unfortunately don't support
it yes yes
oh I have forgot that yes they sell
something Asian soon yes I build a
negation yes so we've got business but
you said earlier that you know you
evaluate formula always in the initial C
in classical temporal yes so what is the
semantics different Allen know is the
same age is that we support formulas of
the shape always be like yes if we're
always evaluating in the initial state
I'll show you all right evaluates the
top level of the formula in the initial
state right but it could happen that
when you say always this means that the
inner part of the formula needs to be a
warranted in all states this is the
semantics of the always operated so from
formula to say formula you change the
point at which you've already right
depending on the semantics of the
temporal operators you change the point
that one of which you evaluate the
formula right so always change is the
point at which you're worried you'll by
borrowing in all points from the current
point onwards and does the
so you have alright form is always nice
you know state okay good so now let's
move on to duster small quick question
next on the box on the left you have
once the previous there's no next
there's your next we don't support it
yes we're somewhat limited but many
things that you can express with next
actually you can express in this way
just you need to massage your formula
but you don't we require always to be
the top level right so never again yes
you cannot think it never again yes this
is always a and ease even maybe simplex
always have rewards you always sorry you
write it down yes we even write it down
in this formulation is contract
authorities all 13 variants exactly and
say this way is but he also can refer to
the positive x service as kind of
coating so this Pierce of why not next I
mean there's there I'm not familiar with
the verification technology so is there
a technical reason why next is more
difficult than previous so for
modifications its item only you need to
do some gymnastics
okay and when you are eventually becomes
more difficult way more beautiful
because once you always look by that
number of steps in the past because in
the past time is limited is bound but in
the future its empowerment when you are
eventually things become ready of their
very infant good okay so maybe we'll
just go quickly order exercises so now
it's time to formalize what we need and
just to solve ours our verifier we have
two servers in which you can remember X
there is an interface let's say this
part of the room uses but X 1 and the
other part of the room is very soon as
can we do it like this because services
power forwards notifications
yes okay ever will the books
[Music]
sorry I've just can't miss vericsson
online too long here's that down with
the Maltese don't like a up
associate in the future don't get your
servers and for verax index you can
treat these things and check out
[Music]
yes
[Music]
okay so so if you open if you open the
links you see this this kind of
interface products on the Left what -
that is the list conflicts posit
specifications so we pre-loaded Maddux
with about context and currently with
office on the ear see plenty when you
see sorry and council right so we have
two contexts which we focus on and the
latest service which solution are the
solutions to those exercises right we
have three extra exercises which you can
do but maybe not maybe that would be no
time for this day now they have no
solutions you need to
[Music]
what was I'm wondering how do you do
these state credit society the state
pretty good success define one as a user
for a sense okay my PC babies maybe yes
so you give police the formulas make
them we'll talk about those remaining
focus but what's important is the first
for me
so the first of all really is your
problem and it has this form always and
then some point so whatever your specify
something and then you have a paper
which gives you more details the seasons
and for example you can refer the
contact is using computers its we can
equal to the context and this way I for
girls family simply sneakers right
also you can refer to my seat sensor you
can refer to the current time and time
yes I guess I stay pretty good spacing I
it's like they will try and you had an
example of like success or refund that's
a big prep it's upon the success fee
around the region on the state for
something done
oh yes
okay let me just give you a short
demonstration about the first property I
taught us my always equals the same
imbalances so
[Music]
okay so it's better we write the first
property right this one is simple same
always
okay
so he's the case that the civil bosses
equals the whistleblowers and but
education thanks subtitle can see that
the property so you need to verification
takes some time so if you know it's not
have to say a two-way get immediately
packages education
like when you have delegated its
you