Player is loading...
Formal verification of Scala programs with Stainless
Friday, June 14, 2019 · 2:20 p.m. · 29m 28s
Everyone knows that writing bug-free code is fundamentally difficult, and that bugs will sometimes sneak in even in the presence of unit- or property-based tests. One solution to this problem is formal software verification. Formal verification allows users to statically verify that software systems will never crash nor diverge, and will in addition satisfy given functional correctness properties. In this talk, I will present Stainless, a verification system for an expressive subset of Scala. I will start by explaining what formal verification is, what are some of the challenges people encounter when putting it into practice, and how it can be made more practical. Then I will give a high-level overview of Stainless, and finally present a few verified programs, such as a small actor system, a parallel map-reduce implementation, as well as a little surprise! I’ll also demonstrate the tooling we have developed around Stainless which lets users easily integrate Stainless in their SBT-based Scala projects.
Embed
Transcriptions
Note: this content has been automatically generated.
00:00:00
oops quick so it's a great pleasure to hear the audience
00:00:06
and enjoyed a that broke so we're gonna talk about discussion that's gonna programs using status
00:00:13
couple was about me or someone which you company and or rob my
00:00:17
computer uh i was a student here in our our with the so contract
00:00:24
we're gonna discuss a few different feelings uh in the prison stainless or
00:00:30
then quickly whether education's about if your intonation and then the mean jeez everything type dresses
00:00:36
then we'll see him for two more case studies of a little buttons features and i'll talk about some of
00:00:41
the other what we like to do with sting us some so i think less is over fusion to for um
00:00:49
programs returns can our up you a subset of skeleton in that we could just gotta
00:00:55
we think it's a fairly expensive subset already so you have this whole
00:00:58
a bunch of features here i want to go over all of them um
00:01:04
but yeah you can see it's already for express it you can like in many many that program with that and uh
00:01:12
i don't and won't use too many fancy types of features you should be should be fine or wanting that's not to be missing here
00:01:18
what is coming soon hopefully is a hard headed types i'm currently working on on this report so i can
00:01:25
follow the bit of history and the notified when we get the seam
00:01:30
you also supports some uh of the dirty features such as uh
00:01:33
depend function type succession at the the topic types but we currently stuck
00:01:38
on that seal point twelve we haven't had time to a great it's got to but that's definitely something we want to look at something
00:01:46
so i still this wonderful in the following way so when you're
00:01:50
according to scan s. your nazi to orson type check the programs
00:01:54
then we extract these programs into our own internal yesterday which we don't know we're down to a a
00:02:00
much simpler language uh from which we generate some vision
00:02:03
conditions that are then passed linux which is the uh
00:02:08
uh solver that doesn't owe a lot of heavy lifting for us and then uh it
00:02:12
it says called into the tree auspices for princess which are set to solve or so
00:02:18
uh so when the lowering of um there's a bunch of a small faces within stainless
00:02:24
that they would have such as the inaccuracies ago was of course muttered lifting
00:02:29
uh we'll swain could type so we'll just make the types we have to include them down too much deeper types that so i don't understand
00:02:36
and uh and so on so what the ones i put in bold other
00:02:39
one that are gonna be used by the examples um and when uh uh presents
00:02:44
regarding i noticed um so i noticed over for a
00:02:48
functional programs but understand the much simpler language than the
00:02:51
than the standard which so we have functions no classes
00:02:55
only any cheese you have been vectors said smell to map
00:02:59
uh quantify ursa just for all or exist and dependent and from
00:03:04
an episode and they're nice we use some quite fancy types that's
00:03:09
um that we used to encode some um some of the more a skylight type so
00:03:15
i won't go into what i next really does it's a lot of magic uh and heavy lifting but
00:03:20
basically i next uh has the discourse ensure that tells
00:03:23
us um reason about recursive functions and things like this
00:03:28
so on the recognition side uh what a stainless allows us to check our
00:03:33
uh some assertions using the standard answer he a function in scandal
00:03:38
you can also opposed conditions to functions in the interim keyword we have precondition is
00:03:43
it require and people can also have a class in volumes on uh on classes
00:03:48
where you can put require within the budget address and we'll check to see that or that is always a true
00:03:56
good example that that's the only uh if i'm asked a question and show
00:04:00
so if you have a function epics in a next of type a and returns would be
00:04:05
you can add this precondition music while you're right the budget the function and then at the poor condition using ensuring
00:04:12
and basically what we can try to do afterwards is try to prove the following a question uh is always
00:04:16
true for any x. whatsoever even if it's an infinite domain like big you'd so yeah we say that um
00:04:23
the precondition worries to to to text inside must imply the post condition apply to the body of the function
00:04:32
so that's basically what stillness is about is about generating such
00:04:35
a fish conditions that are then discharge clients all over itself
00:04:40
we also have some static checks as well uh which also with his job but the solver such as uh
00:04:46
but the matching do stiffness any we kind of got ground was one which is not
00:04:50
them really bad uh partners otherwise division by zeroes are checked rebounds at the main tracks
00:04:57
and few morphine is also like we don't allow quitting and values we we only allow
00:05:03
for initialise valuables in fields we don't support exceptions and more but
00:05:08
actually we check in the frozen over frills on a side integer types
00:05:14
there's also automation checker that comes with stainless uh it's pretty powerful and you poured so
00:05:20
you don't define measures uh of course one elysees central silence when i want want to
00:05:25
details about the nation but it's important for both for a program correctness that also for cruise when
00:05:31
you write proves in stainless wants to prove to terminate otherwise we can basically prove anything you want so
00:05:38
as an example of of a broken uh happen function and least so here i made the mistake of passing
00:05:44
uh and again the recursive call which basically means that happens when you uh for ever
00:05:50
and we should you're going uh see that and will give us an example okay
00:05:55
if you pass this least uh which is the kings of a in another and needed
00:06:00
and new as our then you function will look for ever and so this can
00:06:05
help i hope you would do um and figure out why the functions not terminating
00:06:12
alright main piece of the talk is the recognition of that classes we've
00:06:16
heard a lot about the more useful than going to a a detail about
00:06:20
why they're important for what you should care or not i think we all know that so
00:06:25
they're important and that we should care so here have the standard uh something group type class we've seen many times already
00:06:32
the main difference here is that we can express what's
00:06:36
the efficiency to low ferguson a group directly within the um
00:06:41
but i guess it's repetition but by class and we do this at the when the patient that comes from the students the last library
00:06:47
to instruct stainless that's okay this is a lower you're gonna have to check it
00:06:51
check that is this little holes for um for every instance of the cynical type dress
00:06:57
oh you can also extends from the group
00:07:01
uh and define the mono if just quoted as well you can forget the chip operator
00:07:06
and you can add a couple more hours that have to hold for my now it's
00:07:09
such as left and right identity of empty with respect to come back
00:07:13
and so this is very natural this is that really natural skylark or um
00:07:19
i mean the compatible with some one was the way you expressed those in cats and so on so
00:07:26
it's an it's an x. d. so
00:07:28
now whenever you wanna define an instance here um different instance for a some what happened here
00:07:34
is that a stillness will automatically very fried that the low the laws hold for um for some
00:07:41
uh you have to do anything special a lot that's still as we check it for you
00:07:47
so you would generate something that looks like this that's the rich condition that expressed in the language of i next
00:07:53
any will pass this down quite next that's gonna try to prove that is used to so you see here which is
00:07:59
going to be it's that's we have uh some refinement that since the one that we used to a reason about um
00:08:05
jesus cannot types which are not supported by the scientists over itself and then i
00:08:09
noticed since that's a magic number down the road to to get to remove those um
00:08:15
what you get back utterance to listen this you're gonna get just realise jeez follows is gonna tell you that of course these are
00:08:22
valued because uh some is a proper room my night it's very
00:08:25
fast and it's not that crazy further it's uh it's fast enough or
00:08:31
for having the good the good discipline cycle uh i think
00:08:37
can also define more trusting a one eyed from the other one option
00:08:43
for this you need to have a so the group and you're learning eight that's within g. the option
00:08:48
which you you can then use when you want to combine the two um the to some very some
00:08:54
definitely here uh still as will not be able to prove that's that was all uh for this for this instance
00:09:00
that automatically we have to actually use the fact that uh d. combined operation on the sunny group is it says assertive
00:09:07
we can do but we can in the same definition we can override the lowest
00:09:12
us method which which we defined in the in the sunni group the abstract as
00:09:18
because you for you this little because keyword which is just a keyword from
00:09:22
the our library and then we say okay whenever x. y. and z. also arms
00:09:27
you can use the fact that uh the combined operation on those easy to uh to shoot it and
00:09:33
you should do this then uh students will be able to prove that so this is a decision to them
00:09:42
oh
00:09:46
i think i'm some dislike but yeah well only to show also that's the whole thing that's gonna
00:09:50
who proved by induction so if you define the salute instance phone list um which is just the
00:09:56
uh plus plus what just happened and construct a less to the pool
00:10:01
by induction and it's gonna basically try to but if you do approve
00:10:06
so if x. is real then it's very easy by just
00:10:09
unfolding lois awesome to see that happen operation a decision to
00:10:15
and then it can also performed into t. step in the case for the first argument it comes
00:10:22
and then you can basically find the the to view would right handed flat to
00:10:27
prove little little yourself so we have also dirty reasoning built into some interesting that's
00:10:33
so once we have these you can define for example the form up a function
00:10:38
and you can format policed and some some the element which is so this is called that's the last week which reports and uh
00:10:45
uh you can use as such but now maybe you want to
00:10:49
do something a bit more interesting so just doing this fourteen parallel um
00:10:56
fortunately stillness doesn't really understand uh we don't have support for scallop alright actions
00:11:01
so what you have to do here is you define the aftermath method you convert our own list was
00:11:08
good at least you pull power do the mapping in the fold at this could you back and then
00:11:13
but because they let doesn't understand this dot or operator or you have to do this at
00:11:16
experimentation on the function which is the less likely you don't have to care about the body
00:11:22
you can just the trust that the post condition we added here a wheel was also not here with the stillness
00:11:28
you you have to know that the real substantially the same as a coding the regular sequential format so
00:11:34
that's the thing if you did would some code that we don't support you
00:11:37
have sometimes too and convince yourself that the first condition your writing will withhold
00:11:42
and the but the stats you actually interact with uh with with other libraries could be at yeah you could do
00:11:48
uh the try map the data collection others gonna collection so you can always
00:11:53
but to wrap them in some extent functions and then at those
00:11:55
conditions to to testing us a bit about what this function is doing
00:12:01
so that was for uh like classes uh we have a bunch of all of this to
00:12:05
the the like to mention as well or justin doesn't only do type last lows of education
00:12:11
for example we very five uh come crop implementation which is that the structure that's used
00:12:16
uh for that but by the liberation a good think of it as a it's released but with the good um
00:12:26
with good operation and good performance follow cup of dayton especially happened in preparing them and so using
00:12:32
this we also commented that shouldn't of us prevented a fully by that and verified market this pipeline
00:12:39
but you don't know if that uses these controls and so
00:12:42
on and then you get the fully verified a pal type thing
00:12:48
um jordan's i almost fell from the lab uh also maintaining the uh focused unethical smart
00:12:55
we should both sorting small construction skull i've that's all sort of thing and here you can write to contracts you can reason about
00:13:01
do we need to physically that options are we the which is used in sorry did you for example
00:13:05
which can then generate from scale i can generate thirty to codes that convince you probably and everyone per se or itself uh
00:13:13
variable on pizza but it's your right
00:13:17
and that last even also reason a bit about persistence and so
00:13:21
the one i'm gonna show here is really the a counter with um
00:13:26
backup counter so we have the first primary council just a
00:13:29
dual increases in income message it updated page to the cover to
00:13:34
one and incense to transfer the message but with the backup dancer
00:13:40
which then uh a base it states to do what it says
00:13:43
so this we can model using this is no um d. s. l. we devised which was
00:13:48
a bit inspired by i get that but without the pipe part because we didn't support um
00:13:55
the type messages yet but this would or could be done nowadays um so yeah i define the primary
00:14:01
act or a show the catcher in reference to the backup counters and whenever it gets in the message
00:14:07
it sends the message to the backup counter and we and updated stays with the cancer income to buy one
00:14:14
but the temperatures of the uh the ladder uh just a bit it's it's a increment the counter
00:14:21
and that we can define any point of the system so what what we like to to say is that
00:14:27
something that would be true of all time with the system is that
00:14:30
the value of the primary cancer message equal to devalue the better counter
00:14:38
yeah sure yeah sure so this the backup counters we also have the counter and
00:14:44
whatever gets a nick message just gonna or increment the the value of the counter itself
00:14:49
uh what for me was when we was the save it was just also so sending the message to the um the backup counsel
00:14:56
and so what happens now is that basically the value of the primary control that
00:15:00
was gonna be equal to the value of the backup counter plus the number of messages
00:15:05
that or sense but not just processed by the abides actor so that's
00:15:09
important we like to state of should been doing i in this way
00:15:14
and i want to show that this is true at every step of the systems as a cushion
00:15:20
we can write a little children like this that says that for
00:15:23
such an act of system and to uh references to uh to actors
00:15:27
even volumes was already true for the system if we take us that and
00:15:32
send the message from end to end what an m. d. in the actors
00:15:36
would be primary backup and the primary in itself and so one story whatever
00:15:40
happens with like the volume to hold after the messages in that either the um
00:15:45
and if you'd you'd use to to stay less uh it should be able to prove automatically that so this is the true
00:15:52
in opposing every or respectable system you also have to prove that there was some initial system of this is true as well
00:15:58
and this is just give you basically approved by induction that uh
00:16:02
this important is maintained at every step of the discussion of the system
00:16:06
we also have a little rubber that you can use to run subjects was directly on top of a cap
00:16:11
um which is nice as well i'll have to write your code uh for i guess that's exactly
00:16:16
we could also imagine next uh uh having some deeper integration back yeah but that
00:16:20
hasn't been done yet so um and we have a bunch more code of um
00:16:25
in the balls upholstery and you know what we have a very five one could implementation we have uh we should be
00:16:30
teaching presentation and of course we have left but because there
00:16:33
are no verify fiction systems complete to the left but implementation um
00:16:38
and then as a little buggers ah we actually have if you use the l.
00:16:43
that you from then we have support for a a sofa level of a retirement types
00:16:49
so we didn't touch the type or of dot c. we just added some support for
00:16:52
the syntax and we don't deal ourselves with these requirements are we can stay less so
00:16:57
if you like refinement types you can use those in uh you can write them using the all the different than them
00:17:04
can kind of forget a different us that's that's it
00:17:08
an example of that would be
00:17:11
have a sorted insert function that in certain element into his and
00:17:15
he would require that the list we were given is already sorted
00:17:19
and that the element but i must be smaller than the head of the least either just is not empty
00:17:25
and then we have sorta the result of the operation is a sorted list itself so
00:17:29
yeah i put the two version the one with the acquiring ensuring and on top you have the one with refinements
00:17:35
whichever is better i mean is a matter of taste uh you can basically a pick and choose the in that case
00:17:44
it would do more in talking to haven't we haven't is between acquire plugin which methods
00:17:49
integration but it's good to broke and since we're ready to start to twelve you have to
00:17:55
some work to fix that shouldn't be too hard by the hasn't been done yet people to goes context which is a bit like
00:18:01
that is a restroom but a bit more powerful than general can
00:18:03
stick a stick the goethe edition i'm in more places than every school
00:18:08
we can also do conservation of code and we have a nice decide for writing completely true so as to make the right sometimes
00:18:16
um some features uh i'd like to get into and especially the other one i think you know all
00:18:23
like is the archetypes implementation uh it's kind of halfway there are more too
00:18:29
get done a retirement that's only supported at the top
00:18:33
level of of um definitions movie and they're not propagated
00:18:38
in the in the right way or always so this would like to improve as well and we haven't you
00:18:44
uh action condition generator that's based on a particularly don't for a system that's consistent
00:18:49
before and uh i think there's a reference so on the website to the paper
00:18:54
and then later on we like to also we're suppose connected to fourteen
00:18:59
latest dot c. or um yeah the latest one movie at the time gonna do this not true
00:19:05
gonna haven't we wouldn't be able to match every single release of that c. but didn't do our best
00:19:10
and we were before about not uh the narrative in inner types uh we had the numbers not to check or or uh
00:19:17
two months back but uh one i'd like to bring it back and the uh
00:19:23
anything which it nicely would stay in it so we had that we could use case where you could write
00:19:27
uh basically term level session types and using the you need to check your you had basically
00:19:32
the same guarantee that you would have no language or exception types are and so and so
00:19:39
this is gonna hopefully come out later this year or early next to
00:19:44
also i'm just a small board of of uh people uh
00:19:48
i've been working on this it's the longstanding project will be in ten years almost or maybe more
00:19:54
um and there's a bunch of people in pretty students and others are working on it
00:19:58
i like to paint also our friends at the land has class enter in the triple coat
00:20:03
for the help and advice uh uh in many different uh topics so you want to learn more about ten as
00:20:09
if uh we have a bunch more documentation on line can find that still at that you prefer that's g. h.
00:20:15
and good you sure how to put the or ever have to work with existing codes good shows any party features
00:20:21
i was what does well and does a list of papers you can uh check out one
00:20:25
two or like into the more technical details them and that's what i have um thank you
00:20:41
we ah a lot of time for questions the stock
00:20:46
uh_huh
00:20:49
hi thank you for the top desk right yeah i could you show that that takes ah again
00:20:55
this but before you should use the s. p. d. disquiet just yeah it's fine yeah just uh
00:21:06
or yeah so so i've asked us use e. s. t. u. union types yeah
00:21:14
i know it i mean it actually show that has his is it
00:21:19
yeah so the syntax so what what it says with them for a four
00:21:23
oh the exponential the functions as x. must be of type int and then um
00:21:30
you do the it is empty or that's the standard that's a standard term level expressions or
00:21:35
this is just like it's essentially or actually smaller than the head of the just a heavy
00:21:41
and
00:21:43
and for the return type you have to give a name to the value you return so that's where you have this open open um
00:21:50
but breaks has must be of type stuff in and then uh we want
00:21:55
the result to be sorted or you can uh meets the name of the
00:22:00
of the value in the uh input parameters because we already have a name that's given
00:22:04
by the by the parameter itself so you don't have to the right it twice a week
00:22:12
yeah
00:22:15
i'm more questions
00:22:20
tools for us but we'll have type what you want
00:22:25
just curious how much of a verification machinery sticks around them and
00:22:30
uh actually uh you could you could basically if you use the ghost of the context feature we have which the
00:22:36
and the uh the uh seem to be working again is it a plugin you could basically annotate everything that's approved force
00:22:42
as with that ghost and the video raised enough so you can have really liked the overhead was whatever uh friday for
00:22:49
when you use a certain sharing an acquired those would also stay uh and and the check that from time as well
00:22:54
good what boards uh another version of this functions that uh our market as opposed to
00:22:59
read this period as well so you can basically have normal rent them over at what are
00:23:06
someone old yeah i think you can say
00:23:11
uh_huh
00:23:14
thank you know
00:23:16
yeah
00:23:19
fine i think it's very nice to see these without the vacation or something you know
00:23:28
be they have something to scan as well yeah i wasn't familiar with working yeah
00:23:33
see to say uh you know it's nice to see them so yeah it's kind of one yeah
00:23:40
one day vacation the example you mentioned the thought it
00:23:43
was one of the major thing means your submission minus options
00:23:47
is one more thing because they are the one for something was with
00:23:52
yes each yeah you could make it more fit if you want if you wanted to uh um
00:23:58
for the sorta didn't you could use the we have vision of a curve
00:24:02
but a lot of passion older and so and so you can use these uh
00:24:05
other type classes just under one for ordering right uh uh
00:24:09
but enough it's sort of or a nation that things get
00:24:16
uh_huh
00:24:18
uh_huh
00:24:20
so is everything as statically pool and baseline
00:24:24
or yeah yeah all of potential is uh or aesthetically very five okay thanks
00:24:33
uh_huh
00:24:37
i was asking so if you happen is that like a shopping on
00:24:41
ah base with an architect last uh_huh you can represent the fact that they
00:24:46
they than i actually don't think yeah by that i guess right
00:24:53
yeah yeah exactly okay yeah it's really is that uh
00:24:58
uh from or joey for messenger you mean yeah it's not i mean it
00:25:01
doesn't really uh it doesn't correspond to any a specific it's actually the sense that
00:25:07
if your instance of that elderly uses a is for begins then go use the the
00:25:14
the in their automatic fury but you could like this for nudity and used the jury
00:25:19
and i mean that there's a lot of recording at that goes on behind
00:25:21
the scenes between what you what you see here and what your senses overseas so
00:25:26
uh doesn't was not a specific show you can decommission of different cherries as well or it could be a so it depends
00:25:33
come up with the japanese in that you have a sign that the stacked up
00:25:38
with cell walls yeah okay yeah yeah thank you mean by that but ah
00:25:45
no we haven't had announced uh in a predecessor austen that's that's cool lay on we we
00:25:51
used to have a enlisted had in the in the code is in good and run it
00:25:55
we had the resource down the analysis and everything like this like this we haven't done for
00:26:00
just to see that the structural maybe it was maybe there is this benchmarking the the living
00:26:08
get yeah alright
00:26:13
he
00:26:17
did i
00:26:25
he
00:26:28
okay we can take more one more question i think
00:26:31
i think there was someone found so
00:26:44
or
00:26:49
i think you know i was looking implementation of these in the snow because i i was not mail these basic
00:26:59
oh yeah you begin to look at it looks like seamless calloused
00:27:03
hand something next meeting and it should be some way to configure your
00:27:08
and some rules for example dairies something not to alton mm missions and and you are
00:27:15
not allowed to have initialised misses for example use mostly in the beginning of the project
00:27:22
the question marks something like huh or discourse
00:27:26
in the body often yeah uh_huh and the team
00:27:30
any any she to him be easy able these rules or something
00:27:36
i don't know i'm not at the moment i mean the those
00:27:41
if you wait to customise what's happening with stainless button not uh on the and that's
00:27:45
what the features side so uh that's good to know way too so clearly labelled destructive
00:27:51
you'd have to do it yourself by using the the code that but that's the thing that we could uh at
00:27:56
some point you know lots of initially it's garbage you want to have to look into it and uh we are
00:28:04
so mm easy easy i know she will fail or was it for you it's i'm sorry so
00:28:15
he has passed huh uh_huh so you'll see some linking
00:28:20
mm years ah ah ah tail our present you can run
00:28:25
now and i'll stand so me easy mm mm had this um
00:28:35
and some compiler options to mm mm
00:28:40
mm walton compile run our project or
00:28:45
um what if you can isn't fuse tennis via the s. b. t. plugin
00:28:50
we basically we just talking to the compiler instigators the cheese after type or
00:28:54
so then we we don't stop the competition phase we just report so what we see so that's not gonna brought
00:28:59
the completion of the project is just something you'd have to do it but uses the last time or something like this
00:29:04
uh i mean that's the way it was currently we could change this other node which
00:29:17
yeah it open up yeah
Conference Program
Keynote: Some Mistakes We Made When Designing Implicits (And Some Things We Got Right)
Martin Odersky, Professor EPFL, Chairman Typesafe
June 14, 2019 · 9:13 a.m.
303 views
Brave New World - tales of PureScript and Haskell in production
Felix Mulder, Snoop Dogg
June 14, 2019 · 10:22 a.m.
151 views
Actors Design Patterns and Arrowised FRP
June 14, 2019 · 10:53 a.m.
Taking Resources to the Type Level
June 14, 2019 · 11:48 a.m.
Lord of the rings: the Spire numerical towers
Denis Rosset, researcher in quantum physics
June 14, 2019 · 1:47 p.m.
Formal verification of Scala programs with Stainless
June 14, 2019 · 2:20 p.m.
118 views
Exploring Scala Tooling ecosystem
Jeferson David Ossa, Colombia
June 14, 2019 · 3:12 p.m.
TwoFace values: a bridge between terms and types
June 14, 2019 · 3:43 p.m.
GADTs in Dotty
June 14, 2019 · 4:41 p.m.
302 views
Closing Remarks
June 14, 2019 · 5:49 p.m.
Recommended talks
ScalaClean - full program static analysis at scale
Rory Graves
June 13, 2019 · 10:17 a.m.
463 views
Pure Functional Database Programming‚ without JDBC
Rob Norris
June 12, 2019 · 5:45 p.m.
6375 views