WEBVTT

00:00:00.000 --> 00:00:09.000
and start the recording now and then i'll open up the meeting

00:00:09.000 --> 00:00:15.000
Good morning, everyone. So this is welcome to the Nsf.

00:00:15.000 --> 00:00:22.000
Common methods in the Ppi meeting from University of Pennsylvania, and I'm.

00:00:22.000 --> 00:00:26.000
One of the organizers of this meeting and formal methods in the field.

00:00:26.000 --> 00:00:43.000
It's a it's a program started in the set which has been going on for last 5 6 years, and we are very thankful to the program manages at any step. who started this program, and who have been supporting it over the

00:00:43.000 --> 00:00:54.000
last 5, 6 years, and and then you know i'm not unhappy. So what's this program about?

00:00:54.000 --> 00:01:05.000
So you know many of us, that researchers, informal methods and system design, and the questions that motivate us, and how to specify correctness?

00:01:05.000 --> 00:01:11.000
And these are questions rooted in logical foundations, and how to verify correctness. Where?

00:01:11.000 --> 00:01:18.000
We. We have been working on developing analysis tools to help us students.

00:01:18.000 --> 00:01:24.000
But all of this research makes more sense and it's best done.

00:01:24.000 --> 00:01:38.000
If we have some specific applications in mind and so that's why, that's the motivation for this formal methods in the field program where the field means a specific application domain, and the goal.

00:01:38.000 --> 00:01:46.000
Of the program is to encourage collaborative research between researchers, informal methods and domain experts.

00:01:46.000 --> 00:02:00.000
In in fields. and for the purpose of this Nsf program we have 5 fields, and there are 3 of them operating and distributed systems, network systems and embedded cycle systems.

00:02:00.000 --> 00:02:11.000
And the applications of the methods in these areas that have been developed over the last almost 2 decades.

00:02:11.000 --> 00:02:20.000
And then there are newly emerging areas such as machine learning and human centered computing, which are also part of this program.

00:02:20.000 --> 00:02:31.000
And hopefully, at the end of this meeting we can also think of a new areas where requirement methods could be connected.

00:02:31.000 --> 00:02:35.000
Just just a few minutes regarding the agenda.

00:02:35.000 --> 00:02:41.000
So in the in this opening session we will have docs by

00:02:41.000 --> 00:02:48.000
Margaret and Mattanucci, who is the assistant director of size, and within size.

00:02:48.000 --> 00:02:53.000
There are 3 divisions so ccf is one of them.

00:02:53.000 --> 00:03:02.000
So it's my desktop with the Division director for Ccf

00:03:02.000 --> 00:03:19.000
The lead program director for this program should be the same few months, and then then, maybe that go move on to this term tangled, uniformed methods in industry. and and yeah, the tank phone to a 5

00:03:19.000 --> 00:03:27.000
number. great speakers who have agreed to participate in this nicotine, and from Microsoft David from Meta.

00:03:27.000 --> 00:03:39.000
Actually a chance from networks, from Amazon, and So 5 ppi meeting, we will have then 2 closed sessions.

00:03:39.000 --> 00:03:47.000
So these are open only to the awardies in this program, and you should have got in a link to this.

00:03:47.000 --> 00:03:51.000
The you know the word is when you registered for this.

00:03:51.000 --> 00:03:54.000
So this is going to be in 5 panelist sessions.

00:03:54.000 --> 00:04:09.000
So today 2 to 4 will be a session that there will be liking talks by your bodies, and tomorrow morning there will be an open discussion among the award is in this different groups on success. stories.

00:04:09.000 --> 00:04:14.000
But challenges in their particular area and the new opportunities.

00:04:14.000 --> 00:04:22.000
And these 5 groups will be led by Cindy Fisher and Jennifer in machine learning.

00:04:22.000 --> 00:04:28.000
Diane Stepan, and they call it sandwich on in disputed systems.

00:04:28.000 --> 00:04:42.000
Arthur and Kara to imagine in network systems embedded systems and thrust voting and delay in advancement, in human-centered computing.

00:04:42.000 --> 00:04:46.000
And then all of you who have, you know, join this open session.

00:04:46.000 --> 00:04:52.000
You are welcome again to join the closing session, which will be at 2 Pm.

00:04:52.000 --> 00:05:06.000
Tomorrow, and the same link should work, and we will have again some remarks by the division directors of the other 2 divisions within size of the Intelligence Systems Division, which is led by Michael Litman.

00:05:06.000 --> 00:05:15.000
And the network systems division, then by the deep thing. and, as you can see actually all the how the 3 divisions within size are interested in formal methods.

00:05:15.000 --> 00:05:21.000
So this is this is really great for us, and then we will hear reports from the breakout sessions.

00:05:21.000 --> 00:05:26.000
By the provided by the needs of these 5 sessions.

00:05:26.000 --> 00:05:30.000
So that was about the agenda. And now, let me welcome.

00:05:30.000 --> 00:05:35.000
Margaret Marguerite to a few months.

00:05:35.000 --> 00:05:42.000
Thanks very much. Reggie can never hear me. Okay.

00:05:42.000 --> 00:05:46.000
Can people hear me? We can hear you wonderful I had some audio problems.

00:05:46.000 --> 00:06:00.000
But i'm back wonderful. So good. morning everyone my Name's Margaret Martinosi and I lead the computer and information science and engineering or science Directorate here at the National Science Foundation and I do so as a 4 year term while

00:06:00.000 --> 00:06:09.000
on leave from the Princeton computer science faculty it's nice to see so many familiar faces here in what is such an important topic? area?

00:06:09.000 --> 00:06:15.000
So, as many of you know. but just to sort of reinforce it.

00:06:15.000 --> 00:06:21.000
Nsf is America's Major funder of foundational research across a wide variety of topic areas.

00:06:21.000 --> 00:06:30.000
But nowhere is that more true than in computing where Nsf provides about 80% of the Federal funding for academic research.

00:06:30.000 --> 00:06:48.000
And so obviously it's important for us to engage you the community as we seek to take that really long term view, identify important research opportunities and challenges across many different time frames from blue sky foundational research to other use

00:06:48.000 --> 00:06:54.000
inspired and translational opportunities, and I think formal methods is a great example.

00:06:54.000 --> 00:06:58.000
It has gone through such advances and transformations over the decades.

00:06:58.000 --> 00:07:15.000
And the goal of this particular program is to move the needle into the in on those advances from foundational out into the field to really move the needle on how reliability and security and other topics get taken on in order to

00:07:15.000 --> 00:07:21.000
really fundamentally rethink how we design and build different types of computer and information systems.

00:07:21.000 --> 00:07:28.000
So some of you have heard me tell the story some of you may have all actually been players in the story.

00:07:28.000 --> 00:07:35.000
But i'm a computer architect and so for many years I did the quantitative empirical computer architecture thing.

00:07:35.000 --> 00:07:52.000
But there was a point about 6 or 7 years ago where one of my graduate students really pointed out some of the opportunities to to undertake research using more formal methods, and I was schooled in the matter

00:07:52.000 --> 00:07:58.000
by him by the students that followed by some of my colleagues who are here on the zoom today.

00:07:58.000 --> 00:08:12.000
It has been for me a really transformational set of years to learn about this new tool in my toolkit, and to sort of think about how it can be applied across many different security and reliability. scenarios.

00:08:12.000 --> 00:08:28.000
And so I think what you are doing here today is sort of part of a sequence of many people who, learning because of the work you're doing about these kinds of opportunities from 2,018, and before where there were workshops sort

00:08:28.000 --> 00:08:44.000
of standing up this program to where we are now, after a couple solicitations, really recognizing the way that industry is deploying formal methods. The way that these things are getting taken from theory to practice, I think the goal really

00:08:44.000 --> 00:08:57.000
is to keep it up. and to make sure that the cross pollination of different topic areas occurs so that the topic areas that are really well versed in this can help train the ones that maybe aren't doing it as much to keep making

00:08:57.000 --> 00:09:10.000
that ongoing progress towards our towards our Goals and so with that I'll hand it over now to Dr. Dilma de Silva, who's the lead division director for formal methods in the fields who will

00:09:10.000 --> 00:09:23.000
say a bunch of thank yous i'm i'm going to sort of say a blanket thank you to the program officers and the members of the community who have brought us here together today, and with that Delma over to

00:09:23.000 --> 00:09:28.000
you. thank you, Margaret, so i'm zoom with the sofa.

00:09:28.000 --> 00:09:33.000
I, am a rotator. My home is suspicious. Texas Am.

00:09:33.000 --> 00:09:42.000
University. I joined 3 months ago in the i'm really excited to learn more about the formal methods in the field as a pi.

00:09:42.000 --> 00:09:59.000
I really admire the program, and and I followed in my own research area the papers that were coming across, and the progress that was done in operating systems in particular, which is, I follow, make me very encouraged to be able to work with the

00:09:59.000 --> 00:10:04.000
program directors who are so excited in order to nurture this community.

00:10:04.000 --> 00:10:12.000
So, as Margaret said, by role here is a really farmer, because I got to say thank you, and you know it's really nice, is, I think, Thank you.

00:10:12.000 --> 00:10:20.000
When we mean so much, because thanking the program directors gives me the opportunity just to also highlight.

00:10:20.000 --> 00:10:28.000
How wonderful it is to work with all of them so i'd like to thank Nina Amla because she pioneered all this effort.

00:10:28.000 --> 00:10:44.000
She continues to be enthusiastic about the role that formal methods and formal methods in the field can have and improve our society, and and she takes every opportunity to sell to sell the program to whoever wants to listen

00:10:44.000 --> 00:10:56.000
and in the computing and communication foundations division we have an integral energy Dummy, then Chef and pavita praba car, and these are Pds.

00:10:56.000 --> 00:11:02.000
That I work with daily, but I also work with my colleagues program directors at computer and network systems.

00:11:02.000 --> 00:11:10.000
We have Jaso Halstrom, Daniel Loggeda, Augustine absent, and finally in Iis, which I always forget.

00:11:10.000 --> 00:11:19.000
If it is intelligent information. Sorry, Michael, You have confused bit more because Michael sometimes trips on the name of his division.

00:11:19.000 --> 00:11:23.000
So I, as we have done mostly in waiting. So thank you so much for the program.

00:11:23.000 --> 00:11:29.000
Your actors in my 3 months here, and my admiration for the work that program directors do increase.

00:11:29.000 --> 00:11:35.000
Of course I love them as a pi but i'm really in of what they work for.

00:11:35.000 --> 00:11:38.000
Our what they do for our research community. I end up.

00:11:38.000 --> 00:11:46.000
I saw the rest. cleveland isn't the obvious I couldn't find Kosal russell Rao. but I think he's also a meant to be here.

00:11:46.000 --> 00:12:01.000
And so let me really thank the form of Ccf Division directors who work with the leadership to allocate funds and really nurture the work group that now continues to work with the api So rest

00:12:01.000 --> 00:12:10.000
and cause a Roger. Thank you very much for laying out the in the beginning and getting this going, and I hope you know, to be able to like you.

00:12:10.000 --> 00:12:16.000
Continue to nurture this community in terms of up the commodity itself.

00:12:16.000 --> 00:12:32.000
I'd like to really thank raji valor from U Penn for being, you know, the chair and organizer of all of this, and for the 5 amazing session the session that we have planned for today and for

00:12:32.000 --> 00:12:39.000
tomorrow. I'd like to thank for machine learning sunshit session and Jerusalem for operating and distributed systems.

00:12:39.000 --> 00:12:49.000
Nickel is out of each, and they and Stefan for networking art, Gupta and Ratu Mahjan and for embedded system.

00:12:49.000 --> 00:13:04.000
Cyan Metra, and, like me, Jose and finally for human-centered computing Raspberg in Elena Glassman. Sorry if I miss pronounce too badly your name but really thank you and i'm looking forward

00:13:04.000 --> 00:13:09.000
popping up in many of those sessions, and and and hearing the discussion from the Apis.

00:13:09.000 --> 00:13:15.000
Finally our audio minist staff, Antonio coordinates Anita Tyler and Nato.

00:13:15.000 --> 00:13:20.000
William really worked closely and made all this happen. So thank you very much.

00:13:20.000 --> 00:13:26.000
And of course, thank you also the it support that we are all you know benefiting from now.

00:13:26.000 --> 00:13:31.000
So. Thank you. Thank you. Thank you. pavitra!

00:13:31.000 --> 00:13:41.000
Nina, I passed to you so that you go to the next person

00:13:41.000 --> 00:13:55.000
Great. thank you, don'tma and margaret for your remarks and reg for your intro alright so i'm puppetrack rabaker i'm a program director in the computing

00:13:55.000 --> 00:14:01.000
and communication foundations division, which is within the computer and information, science and engineering direct rate.

00:14:01.000 --> 00:14:16.000
So Dilma is our division head and Margaret is our directed, and i'm a rotator from Kansas State University, where I do research on cyber physical systems, formal methods.

00:14:16.000 --> 00:14:21.000
And ai. so applications or formal methods to Cps and Ai.

00:14:21.000 --> 00:14:33.000
Essentially so, Michael today is, to give a brief overview of the kind of awards that we have done as part of this program.

00:14:33.000 --> 00:14:36.000
And to briefly talk about the goals of this Pi meeting.

00:14:36.000 --> 00:14:50.000
So You've already put it. very Well, the formal methods in the pro Fields motivation was mainly based on the statement from Miller's thesis which emphasize this bidirectional

00:14:50.000 --> 00:14:58.000
interaction between theory and practice. We want theory to be informed by practice, and we want practical systems to be built based on strong theoretical foundations.

00:14:58.000 --> 00:15:05.000
So there was this market divisional effort within size, and where the Ccf.

00:15:05.000 --> 00:15:19.000
Cns and is division came together to support this program, whose broad motivation was to build reliable, robust, and resilient software systems as well as to build this community of researchers that could support this aim where we had

00:15:19.000 --> 00:15:30.000
researchers from formal methods as well as those from the fields, working symbiotically towards building, towards doing research that enables reliable and resilient software systems.

00:15:30.000 --> 00:15:35.000
So we are currently in the second iteration of this program.

00:15:35.000 --> 00:15:52.000
And the next call, which is the last call as part of This iteration is in February of 2,023, and Raj. you already touched upon the 5 areas that we have been it's soliciting proposals in as

00:15:52.000 --> 00:16:02.000
part of this program, which is machine learning, operated distributed systems, networks, embedded systems, and human compute centered computing.

00:16:02.000 --> 00:16:09.000
But we have all this encouraged proposals from field areas which are beyond these 5 that have been listed, and I will.

00:16:09.000 --> 00:16:19.000
I will touch upon those as well. So I want to give a brief overview of the kind of or the breadth of topics that have been

00:16:19.000 --> 00:16:26.000
Funny through this program. So here is an overview of the different

00:16:26.000 --> 00:16:38.000
This chart basically summarizes or clusters the different words that come up in the titles of the awards made so far, and you can see that all the 5 areas are very well represented.

00:16:38.000 --> 00:16:42.000
In this picture I will flash a slide for each of the areas.

00:16:42.000 --> 00:16:46.000
Just to give an example of the kind of awards we have done so.

00:16:46.000 --> 00:16:50.000
For instance, in networking we have a formal method.

00:16:50.000 --> 00:17:06.000
Various kinds of formal method techniques being investigated through program synthesis, verification, satic and dynamic analysis being applied to different applications of networking, including generating update controllers verification of condition control

00:17:06.000 --> 00:17:22.000
algorithms and monitoring of data planes, and so on. When When we come to operating systems, again, we have verification methods based on types, systems, smt solvers, symbolic execution techniques being applied to verify operating

00:17:22.000 --> 00:17:27.000
systems as well as composition techniques being applied to verify distributed systems.

00:17:27.000 --> 00:17:32.000
In the context of machine learning, we have awards that these would explainability.

00:17:32.000 --> 00:17:48.000
We have awards that look at efficient transformations of neural network or market architectures to enable scalable verification as well as specification and verification for newer classes of system machine learning, systems like generative

00:17:48.000 --> 00:17:55.000
adversarial networks, in fact, with applications to things like medical imaging, and so on.

00:17:55.000 --> 00:18:07.000
In the context of embedded systems we have formal methods being applied to autonomous and semi autonomous vehicles, using some advanced predictive analytics verification of embedded system

00:18:07.000 --> 00:18:16.000
compilers and verification and program synthesis being applied to hardware default analysis In the context of human-centered computing.

00:18:16.000 --> 00:18:22.000
Again, we have formal methods being used to eliminate and minimize human interaction errors.

00:18:22.000 --> 00:18:32.000
To build software tools that can help people interactively program and correct back construction, kind of methods being applied to experiment as design.

00:18:32.000 --> 00:18:40.000
So these for the 5 areas. But in addition to the traditional research programs, we have also funded.

00:18:40.000 --> 00:18:47.000
Summer schools and transition to practice a kind of proposals that advanced tool building.

00:18:47.000 --> 00:18:55.000
So many of us. No shankar network has been running the formal math at summer school for over a decade.

00:18:55.000 --> 00:19:01.000
Now, and in the last few years he has also organized the formal methods in the field boot camp.

00:19:01.000 --> 00:19:15.000
Along with these summer schools, which aim to train students in the applications to formal methods, and this has been an extremely beneficial event for students all over the Us.

00:19:15.000 --> 00:19:25.000
Especially for those that come from institutes, which don't have a strong formal methods group, or who don't have access to a lot of formal methods courses.

00:19:25.000 --> 00:19:33.000
So we We are truly thankful to Shankar for organizing this events, and this is a great

00:19:33.000 --> 00:19:41.000
Give back to the community. So, in terms of the transition to practice a kind of proposals, we have tool.

00:19:41.000 --> 00:19:51.000
We have supported tool building efforts in the area of neural network verification into integration of smt solvers to proof assistant formal reasoning for legal conveyances.

00:19:51.000 --> 00:20:09.000
As I said, this is just you know, a pick and choose a couple of topics that from the wide range of proposals that we have funded, and in addition to the 5 areas that we mentioned we have also funded proposals in

00:20:09.000 --> 00:20:12.000
field areas like synthesizing quantum circuit compilers.

00:20:12.000 --> 00:20:18.000
The verification of computational physics and synthesis of microfluidic chips.

00:20:18.000 --> 00:20:23.000
So finally, to sort of summarize the goals of the Pi meeting.

00:20:23.000 --> 00:20:27.000
We are here to learn about the different projects that have been funded.

00:20:27.000 --> 00:20:33.000
So we have lightning talks. being given by almost all of the awards from the program.

00:20:33.000 --> 00:20:36.000
We look forward to cross fertilization of ideas.

00:20:36.000 --> 00:20:48.000
We have experts here, from formal methods broadly defined as well as the field areas, and really look forward to collaborations and cross fertilization of ideas.

00:20:48.000 --> 00:21:01.000
And finally, we are looking forward to identifying challenges and next steps for the broader adoption of formal methods. And we hope to see a lot more discussion on this during the breakout sessions.

00:21:01.000 --> 00:21:05.000
And yeah, we look forward to interacting with you today and tomorrow.

00:21:05.000 --> 00:21:14.000
Thank you. and I think back to Regina

00:21:14.000 --> 00:21:22.000
Yeah, Thanks. Thanks. So I think we are about 5 min ahead of schedule.

00:21:22.000 --> 00:21:32.000
But the but let's get started with the next next item on the agenda, the the industry panel.

00:21:32.000 --> 00:21:57.000
So we have 5, and this So let me actually just bring up Max Slide 8

00:21:57.000 --> 00:22:20.000
Yeah. So So this this panel brings fun with my test experts who are currently working in the industry and trying to transition some of the ideas in common methods to actually impacting the practice of system design

00:22:20.000 --> 00:22:30.000
in in in the street, and super. So let me just introduce them, and then we will have short presentations by each of them.

00:22:30.000 --> 00:22:36.000
And then they will have questions announces, So the first analyst is a nickel. My owner.

00:22:36.000 --> 00:22:54.000
Who is at Microsoft Research. So So Nikolai is work with but the empty solvers, particularly one of the designers of Z 3, which is used widely, and he has been working with applications to

00:22:54.000 --> 00:23:00.000
network systems recently. Alright. So thank you.

00:23:00.000 --> 00:23:12.000
Our next panelist is David Jeff, who was a professor at Stanford for many years, and is now at Meta, and he has been developing business.

00:23:12.000 --> 00:23:19.000
Building a group cryptocurrencies and reliable programming.

00:23:19.000 --> 00:23:23.000
Thank you, Dave, for participating in Theana.

00:23:23.000 --> 00:23:35.000
Actually, Iraq is at math books and action is working on, designed to embedded control systems and cyber physical systems.

00:23:35.000 --> 00:23:44.000
And he has been trying to push on the methods and products which are used widely in the in industry.

00:23:44.000 --> 00:23:51.000
So, thanks actually. but Inevita, who is a leader at aws

00:23:51.000 --> 00:23:59.000
So the end of Us program group is now kind of a good to place for many of the internal methods.

00:23:59.000 --> 00:24:09.000
And they have been working on. Okay? how? how do they? How to give security guarantees in in cloud?

00:24:09.000 --> 00:24:16.000
You think and thanks they have for taking time to participate in the panel. And what is the game for?

00:24:16.000 --> 00:24:23.000
You know. Oh, who has been working on programming that take me on for many decades, but is now.

00:24:23.000 --> 00:24:34.000
I had set around trying to transfer some of this technology to Oh, the distributed systems and smart contracts.

00:24:34.000 --> 00:24:41.000
And thanks. Thank you for joining. I saw. So the plan for the you know, for the rest of the session.

00:24:41.000 --> 00:24:54.000
Is that each each one of them will give us Some of the sexes can formal methods in that industries of some of the challenges.

00:24:54.000 --> 00:24:58.000
And then also some of the opportunities and advice to academically.

00:24:58.000 --> 00:25:05.000
So just in this area. if you have any questions please type them in the chat.

00:25:05.000 --> 00:25:11.000
So i'll be monitoring the chat and you know i'll ask them at suitable times, and after the presentations.

00:25:11.000 --> 00:25:18.000
We also have, hopefully, time for an open Q and a session.

00:25:18.000 --> 00:25:21.000
So me so, Nicolai, do you want to go first?

00:25:21.000 --> 00:25:34.000
Yeah, Can you allow me to share my screen? Thank you.

00:25:34.000 --> 00:25:41.000
The slides up. Yeah. Okay, So I i'll try to keep it with 10 min.

00:25:41.000 --> 00:26:04.000
So So former methods from the perspective of Microsoft research research software engineering comprises of a large number of tools, and we have over the years built tools and interacted with product groups and external on

00:26:04.000 --> 00:26:21.000
deploying and using these tools so here's an overview of the range that the tools target, so they they target areas from designs to implementation testing deployment, and and also aspirational diagnosis

00:26:21.000 --> 00:26:31.000
and the the tools listed below the line are mostly recent tools.

00:26:31.000 --> 00:26:39.000
That's a longer history of those and and also the the tool that I mostly work on is not listed.

00:26:39.000 --> 00:26:49.000
Here is the underlying most of these tools that's switch somewhere on the side is not directly tied to a scenario.

00:26:49.000 --> 00:27:05.000
So a summary of the various areas that Microsoft Research groups have been involved with This is given here in the following slides: Okay, go over them in in more detail.

00:27:05.000 --> 00:27:23.000
But just from the overview there's, some major areas of symbolic model, checking and model-based testing of model programs, systems, code, verification, concurrency, testing, fuzzing, and network with So symbolic model

00:27:23.000 --> 00:27:35.000
shaking started with the slam project around 2,001 and 1 one thing to

00:27:35.000 --> 00:27:43.000
So. So the impact of that was in in shaping in the static driver. Verifier

00:27:43.000 --> 00:27:49.000
But one thing to notice I want to make an notice of in this overview.

00:27:49.000 --> 00:27:54.000
Is that it was influenced by work developed in academia.

00:27:54.000 --> 00:28:03.000
So predicate abstraction influence the the way that Islam static driver verifier operated.

00:28:03.000 --> 00:28:08.000
Similarly, there's a thread around a constraint work closes.

00:28:08.000 --> 00:28:24.000
And the solving methods were that that i'm employed in set threes or cost solver were influenced by collaborators.

00:28:24.000 --> 00:28:37.000
On on ic 3, and there's another angle, which is that the current home class solver is is is a component of set 3, but also it developed in academia.

00:28:37.000 --> 00:28:43.000
So there's an academic angle in an insider.

00:28:43.000 --> 00:28:55.000
Now model based testing has been pursued as long in different guises the 3 most recent are called Bask Iv.

00:28:55.000 --> 00:29:05.000
And sin The targets various different domains past Targets Cloud Api Contracts Iv.

00:29:05.000 --> 00:29:18.000
Targets Iv: rfc's specifications and and basically does specification exploration and sin is used in network verification.

00:29:18.000 --> 00:29:32.000
There's the systems code verification has been very prolific and with 2 angles, one based on the boogie tool chain that has given been foundation for many program verification. tools.

00:29:32.000 --> 00:29:53.000
It's a verification condition, generator but it's There's a different thread around that takes a starting point functional programming and logics and that's a has been a a threat with if star as as a

00:29:53.000 --> 00:30:01.000
main language, but there are many others. one of the Miros is targeting a rust verification.

00:30:01.000 --> 00:30:05.000
For example, this very recent collaboration with Cmu and Syracuse?

00:30:05.000 --> 00:30:18.000
So some of the one of the success stories I like to talk about in the context of the verification is the use of probably correct low-level parser.

00:30:18.000 --> 00:30:24.000
So prior to deploying the hypervisors with ever parse.

00:30:24.000 --> 00:30:34.000
Historically, 30% of the bugs that were uncovered or have been uncovered in the hypervisor, which have been in the parsing.

00:30:34.000 --> 00:30:53.000
And now they're none. there there's also a thread around cryptography and and here's a chart of verifying assembly code versus synthesized cryptographic

00:30:53.000 --> 00:30:59.000
code. So this this assembly call is almost half an order of magnitude faster

00:30:59.000 --> 00:31:06.000
In terms of throughput than the then the high label, Cryptographic Primitives.

00:31:06.000 --> 00:31:18.000
But this also verified So that has had impacts both in Microsoft and Non Microsoft products.

00:31:18.000 --> 00:31:25.000
So, for example, there are components of the Linux kernel and firefox browser.

00:31:25.000 --> 00:31:31.000
Using these verified cryptographic and libraries concurrency testing again.

00:31:31.000 --> 00:31:49.000
It has a prehistory of with very soft and and spin that aimed for stateless resp. enumerative state space exploration, and within microsoft it has a

00:31:49.000 --> 00:32:05.000
evolved over a different technology. So with chess and cars systems, it evolved from using systematic schedule expiration into randomized scheduling.

00:32:05.000 --> 00:32:09.000
The main tools today are called torch and Coyote.

00:32:09.000 --> 00:32:20.000
And they target development and testing modes. So coyote, just, in short, is deployed since 2,017.

00:32:20.000 --> 00:32:25.000
First it was had a self-contained language for state machines.

00:32:25.000 --> 00:32:30.000
They need was in 2,000 made dot net intrinsic.

00:32:30.000 --> 00:32:34.000
So you could that programming dot net and more squeezedly.

00:32:34.000 --> 00:32:40.000
Your target C programs is used in various clouds services.

00:32:40.000 --> 00:32:53.000
Torch is used in is an internal tool at coyote is open source torch is internal runs for testing it.

00:32:53.000 --> 00:33:01.000
It re it reverse engineers concurrency primitives to say it's in a rough way, and it's one.

00:33:01.000 --> 00:33:11.000
It finds box for various agnostic of the applications fosing again

00:33:11.000 --> 00:33:17.000
And a started with dart and cute

00:33:17.000 --> 00:33:26.000
And it is this day going strong, with a wrestler and and hyperfos that I will just mention.

00:33:26.000 --> 00:33:33.000
Briefly, Wrestler is a api forcing tool that fuses web services.

00:33:33.000 --> 00:33:40.000
It's open source. hypervisor is an internal tool that was built for fuzzing the

00:33:40.000 --> 00:33:51.000
Again the hypervisor virtual machine it uses symbolic execution and and set 3 theorem proving to find bug paths.

00:33:51.000 --> 00:33:59.000
It found 11 bucks and and that's in a in a component with a bounty is a quarter of 1 million dollars.

00:33:59.000 --> 00:34:17.000
Network. verification is a larger area that where we have invested to the past decade one of the tools takes routing forward in in in data centers with lots of queries of correctness checks done

00:34:17.000 --> 00:34:21.000
on the fly every day on hundreds of thousands of routers.

00:34:21.000 --> 00:34:29.000
It. and your development is a domain specific language for writing these checkers.

00:34:29.000 --> 00:34:35.000
It's called zen spark isn't is a way of getting configurations.

00:34:35.000 --> 00:34:54.000
And these tools are then integrated in a what's called a network change verification system that is used in deployments of new configurations so-called network repaves which are major sources of potential

00:34:54.000 --> 00:35:07.000
major outages, and so far it's been running in a couple of years now, and the verified hundreds of migrations, and prevented outages every quarter.

00:35:07.000 --> 00:35:21.000
It prevents. what could have been significant outages so that's my summary

00:35:21.000 --> 00:35:39.000
Thank you. the the call, if you have any, give me a question when you collide, is, you know, type in in chat. but we will have also plenty of time for our questions how about specific

00:35:39.000 --> 00:35:45.000
documents, but also, you know the broader questions about adoption of formal methods.

00:35:45.000 --> 00:35:50.000
At the end of all the talks we will have vital discussion.

00:35:50.000 --> 00:35:55.000
So yeah, I I don't see any talk so let's let's move to the next month.

00:35:55.000 --> 00:36:04.000
So yesterday your next

00:36:04.000 --> 00:36:11.000
Hi! I realize I've usually had a struggle getting the slides to show in the right way.

00:36:11.000 --> 00:36:20.000
So. let me quickly I think maybe i'll just get presentation mode, and so show the the slides is there edited?

00:36:20.000 --> 00:36:37.000
Hang on a second. Okay, So actually they would set it slides.

00:36:37.000 --> 00:36:43.000
There are 2 questions for you as a from June.

00:36:43.000 --> 00:36:48.000
Does Microsoft use only their own tools what about other open source tools?

00:36:48.000 --> 00:36:53.000
I I didn't catch the last part of the question with my Microsoft users.

00:36:53.000 --> 00:37:00.000
What Do you just use your own tools, or do you also use other open source?

00:37:00.000 --> 00:37:11.000
Microsoft uses open source tools. I I presented it from the perspective of Microsoft research that develops tools as well.

00:37:11.000 --> 00:37:26.000
Microsoft as a company uses open source so for example. there's an infer there's an infer adaption, which is from the major as as one example.

00:37:26.000 --> 00:37:35.000
And then answer the question, how do you handle training? But, efforts in Microsoft training depends on.

00:37:35.000 --> 00:37:48.000
So so depends on the tools and groups, so for example, they're training in Tla plus driven by Marcus Cooper, who develops an old steel a plus tools. there.

00:37:48.000 --> 00:37:54.000
So some of the interactive tools have associated training on others.

00:37:54.000 --> 00:38:01.000
It's more peer pure training or period oriented.

00:38:01.000 --> 00:38:12.000
So there's no training for set 3 for example. Okay, so is my is my screen halfway legible.

00:38:12.000 --> 00:38:24.000
Yes, yeah, we can see here at the screen. Okay, so I can't give a sweeping overview of formal methods work at at Meta.

00:38:24.000 --> 00:38:34.000
I have been. it is not as extensive as Microsoft or Amazon which are really the industry leaders and applied formal methods, at least among large companies.

00:38:34.000 --> 00:38:45.000
So there are scattered efforts here. and there and i'm going to talk about what I know, and the project I worked on for 3 years, which is the development of the Move prover, which is a formal verification system, for smart

00:38:45.000 --> 00:38:51.000
contracts, and so i'll give a little background on where the project came from.

00:38:51.000 --> 00:38:56.000
Talk about what we did, and some of the things we learned.

00:38:56.000 --> 00:39:13.000
So. yeah, So i'll mention also that I can't claim that this is and on ambiguous success story, because, in fact, the project was was cancelled at meta i'll talk about that a little bit

00:39:13.000 --> 00:39:24.000
more. but the move prover still lives it's an open source project, and it is being used by some Spin-offs from Meta and other companies that are using the infrastructure that we developed so this was part of

00:39:24.000 --> 00:39:31.000
the Libra Dm Project at Facebook which there's a lot of renewing that's got on here, which is already a bad sign.

00:39:31.000 --> 00:39:39.000
But at at Meta now and so and I think 2,018.

00:39:39.000 --> 00:39:48.000
There was an ambitious project conceived, and I think it was launched in mid 2,019, with great fanfare, and got a ton of publicity.

00:39:48.000 --> 00:39:52.000
So it was to build a blockchain to serve the financially underserved.

00:39:52.000 --> 00:40:04.000
So more than half of the world population. doesn't have bank accounts, for example, and we were targeting people who are not served well by the current financial system. or That's what we hope to do.

00:40:04.000 --> 00:40:13.000
And so we built a system from scratch, a whole new blockchain, whole new cryptocurrency, based on large-scale Byzantine consensus.

00:40:13.000 --> 00:40:21.000
No proof of work. We developed a new language for programming smart contracts called the Move language, and that was intended to be formally verified.

00:40:21.000 --> 00:40:35.000
And so, as part of the project, we developed the move prover i'll mention that the interest in formal verification really came from one guy who's leading the manager who recruited the team to do the the language and whatever and I

00:40:35.000 --> 00:40:44.000
think, you know, I went around our organization at some point and got questions from senior engineers like what's formal verification.

00:40:44.000 --> 00:40:49.000
So there's kind of one visionary who was pushing for this, and recruited and assembled the team to work on it.

00:40:49.000 --> 00:40:56.000
The project was ultimately never launched. It was actually formally canceled this year. the reason seem to be non-technical.

00:40:56.000 --> 00:41:03.000
And I they're above my pay grade so it's regulatory problems of an unspecified nature.

00:41:03.000 --> 00:41:10.000
But the system was fully open source, and there are 2 startups that are both supposedly worth over a 1 billion dollars.

00:41:10.000 --> 00:41:24.000
Now The form from the technology and some of the staff of the project and the move language of the move prover are still used by these startups and a few other companies outside Meta.

00:41:24.000 --> 00:41:33.000
So I wanted to. You know I spent a lot of time thinking about what we were trying to do is hard and their their known failures.

00:41:33.000 --> 00:41:36.000
And so why did we think that this project might be successful?

00:41:36.000 --> 00:41:47.000
One of the reasons was the need for it. So that already been a track record of hundreds of millions of dollars in losses from bugs and smart contracts, and those losses have escalated since then.

00:41:47.000 --> 00:41:56.000
So. So there's basically smart contracts in a blockchain, which i'll say for people who aren't into blockchain land is just something that updates the state of the blockchain.

00:41:56.000 --> 00:42:01.000
So basically the most important financial transactions are handled by software which are called smart contracts.

00:42:01.000 --> 00:42:07.000
So that said, These things are a high assurance system by which there are many definitions out there.

00:42:07.000 --> 00:42:20.000
I will say something that is designed to have a low likelihood of major failures, which in this case would be inability to use the blockchain, or, more importantly, large financial losses.

00:42:20.000 --> 00:42:24.000
So blockchain should be and aren't always high assurance systems.

00:42:24.000 --> 00:42:32.000
There are large amounts of assets. at stake transactions are hard to reverse compared with banks or the traditional financial system.

00:42:32.000 --> 00:42:41.000
It's the kind of usually open source and whatever so it's likely to be targeted by highly motivated and well-resourced adversary.

00:42:41.000 --> 00:42:46.000
So you can see the complete design of the system, and there have been large losses already.

00:42:46.000 --> 00:42:50.000
The Move programming language was conceived by others at Facebook.

00:42:50.000 --> 00:42:57.000
It was already well under design by the time I got started and It's a programming language for implementing smart contracts on the Dm.

00:42:57.000 --> 00:43:07.000
Blockchain. It is designed for safety. not specifically to enable formal verification, but the formal verification team had some input into the design of the language.

00:43:07.000 --> 00:43:15.000
A module and move can only be call. You can only call modules that already exist, so that eliminates

00:43:15.000 --> 00:43:32.000
A number of problems, including the ranchancy problems that are famous in more traditional blockchains with the solidity, programming language. And one of the most novel thing about move is a resource type which models physical

00:43:32.000 --> 00:43:37.000
assets. So it's a value that cannot be deleted or copied outside of the module that defines it.

00:43:37.000 --> 00:43:41.000
So the move Language has limited expressive power which is good for formal verification.

00:43:41.000 --> 00:43:45.000
People there are references, but they can't be stored permanently.

00:43:45.000 --> 00:43:51.000
They're only they can only be kept in local variables and passes parameters there's really effectively.

00:43:51.000 --> 00:43:56.000
No aliasing which is enforced by static analysis of the programs.

00:43:56.000 --> 00:44:06.000
There are no first class procedures and no dynamic dispatch, so it has fewer hard problems than many languages for formal verification.

00:44:06.000 --> 00:44:11.000
The move prover is really a traditional employee, horse-style, verifier.

00:44:11.000 --> 00:44:15.000
So the idea is that you write specifications in the form of pre conditions, post conditions.

00:44:15.000 --> 00:44:23.000
In our case, global invariance. and for the move prover, the front and technology dealing with the semantics, the language.

00:44:23.000 --> 00:44:33.000
We implemented our group, but we made heavy use of off the shelf technology, and in fact, the project would not have been feasible without that.

00:44:33.000 --> 00:44:36.000
And so we relied on existing S. and T. solvers, particularly Z.

00:44:36.000 --> 00:44:44.000
3 and Cvc 5, and the boogie intermediate verified language.

00:44:44.000 --> 00:44:56.000
Yeah, which we may change as to Boogie and We worked with a Clark Barrett's group at Stanford, and the group of the University of Iowa, to get changes in Cvc 5 to make it more

00:44:56.000 --> 00:45:01.000
suitable for the task. So this is a really hard project.

00:45:01.000 --> 00:45:06.000
I mean people have been working on floyd horror verification since Floyd and Horror were inventing it.

00:45:06.000 --> 00:45:14.000
And so that's something like 60 or 70 years and it's tough. but we felt we had some keys to success.

00:45:14.000 --> 00:45:22.000
The the make it worth ItNo. Only today. Okay. please.

00:45:22.000 --> 00:45:29.000
Mute, I guess. So we were starting with a clean, slight which is pretty unusual in industry.

00:45:29.000 --> 00:45:36.000
We tried to avoid problems with verifying traditional software, such as programming languages that were very complicated or ill-defined.

00:45:36.000 --> 00:45:40.000
We weren't dealing with a legacy programming language in this case.

00:45:40.000 --> 00:45:48.000
I was pushing for a methodology, and I may not have been successful where we verify as we go.

00:45:48.000 --> 00:46:00.000
So instead of somebody designing and writing code and then tossing it over offense for a verification team to work on, we hoped to have the verifier be a part of the development process, and in a lot of the world

00:46:00.000 --> 00:46:13.000
There's not that great a concern with bugs but there's ample reason for people in the smart contract world to be concerned about bugs, because the losses are quantifiable, and have killed many businesses and so we are also

00:46:13.000 --> 00:46:23.000
co-designing the tools, the problem, programming style, and the verification method, dialogy together to try to maximize our chances for success.

00:46:23.000 --> 00:46:27.000
So the results of the project at Meta. This is before

00:46:27.000 --> 00:46:43.000
It started being used externally. Where do we? All of the the really the business logic and the the foundations of our blockchain were implemented in the move programming language, And we wrote extensive specifications for the move

00:46:43.000 --> 00:46:51.000
infrastructure. So it's called the Dm. framework, and so we specified and verified all of the access control requirements for which there existed a public document.

00:46:51.000 --> 00:46:59.000
And the specifications pointed back to that, and we found several bugs in the process of doing that had much more confidence in our access control.

00:46:59.000 --> 00:47:05.000
After doing it. we specified and verified the documented abort conditions and transcripts.

00:47:05.000 --> 00:47:11.000
In transaction scripts we so in a blockchain.

00:47:11.000 --> 00:47:14.000
Transactions are atomic and can abort. and so we check that.

00:47:14.000 --> 00:47:18.000
The documentation was accurate, and we specified many other properties as well.

00:47:18.000 --> 00:47:24.000
What we're most proud of is that These specialifications could be used during continuous integration.

00:47:24.000 --> 00:47:36.000
So anytime that somebody checked in their changes, we would rerun formal verification on them and flag anything where a change in the code or a change in the specification or anything else in the environment caused verification to fail and so

00:47:36.000 --> 00:47:41.000
verification worked reliably enough and quickly enough that you could just push a button.

00:47:41.000 --> 00:47:49.000
Wait a minute or 2, and it would finish so this stuff is all open source, and it's all out there in github repositories.

00:47:49.000 --> 00:47:56.000
I think it's called moved, dash language at the moment the prover source code is out there, too, as is documentation.

00:47:56.000 --> 00:48:09.000
I still think it's in a preliminary state or other people using it, and I, I wish the project had been able to continue for a couple of years at Meta with the working on it, so that we could have taken on some

00:48:09.000 --> 00:48:14.000
of the remaining challenges. So let me talk about some of those challenges.

00:48:14.000 --> 00:48:20.000
So. You know. One of the great things about working on industry in a project is that you can't dodge problems.

00:48:20.000 --> 00:48:32.000
I mean one of the great things about working in academia is, you can redefine the scope of your research to do whatever is most likely to have the maximum impacts in industry.

00:48:32.000 --> 00:48:37.000
You. Finally, I have to confront all those problems where you in my case.

00:48:37.000 --> 00:48:42.000
I've worked in both kick the can down the road in academia, so we don't want to worry about that problem.

00:48:42.000 --> 00:48:50.000
You'd actually have to worry about it in industry so I feel that this kind of formal verification where specifications are written.

00:48:50.000 --> 00:48:58.000
And you're actually trying to prove the correctness of code has to be part of a programming the program development methodology.

00:48:58.000 --> 00:49:06.000
So systems have to be designed for formal verification. the hardest thing you're gonna do with a program is formally verified.

00:49:06.000 --> 00:49:11.000
And so the programming language and everything else ought to be optimized for formal verification.

00:49:11.000 --> 00:49:24.000
Not something where you write it for speed, or you know ease of programming. and then let somebody else deal with the formal verification problem, because that makes formal verification even harder when it starts off being the hardest problem.

00:49:24.000 --> 00:49:31.000
So i've looked at the design of safety critical systems fairly closely in another context, and it's like incredibly costly.

00:49:31.000 --> 00:49:39.000
It works, you get systems that are actually safe, say for avionics, but at incredible cost in time and delay.

00:49:39.000 --> 00:49:47.000
So I think the challenge before us, in formal verification for critical systems is to figure out, How can you do it at?

00:49:47.000 --> 00:49:58.000
You know, necessarily more cost than normal development processes, but at a fraction of the cost that the methods we use for safety critical systems entail

00:49:58.000 --> 00:50:15.000
So other challenges. you know, you got, in this case a system which requires somebody to write specifications, writing, debugging, and testing of coverage and specifications is is something that at least in the software area is not an advanced

00:50:15.000 --> 00:50:23.000
art, and we put some work into that. we would have put more work into it, and it's an area that I think deserves further exploration.

00:50:23.000 --> 00:50:26.000
I think we had some fairly good ideas for that. They were preliminary.

00:50:26.000 --> 00:50:30.000
We just had them explored by an intern smt!

00:50:30.000 --> 00:50:39.000
Solvers still are not perfect. I mean we're relying on 20 years of prior work, and actually truly amazing programs.

00:50:39.000 --> 00:50:46.000
I got in on the ground floor working with smt solvers and I really can't believe how much better Z.

00:50:46.000 --> 00:50:52.000
3 is than the it was, you know, 10 years ago, or the the programs I used in the past were so.

00:50:52.000 --> 00:51:01.000
Those advances enabled this, but there were some deficiencies, and we were surprised to discover the reasoning about vectors was actually difficult, given.

00:51:01.000 --> 00:51:07.000
How commonly used vectors are in programs. One of the things we did was collaborate with the Cvc.

00:51:07.000 --> 00:51:17.000
Team at Stanford and the University of Iowa to develop a special theory of vectors and supports concatenation, and as well as indexing into finite length vectors.

00:51:17.000 --> 00:51:22.000
And they actually published a pretty good paper on that last summer.

00:51:22.000 --> 00:51:39.000
Generating small, meaningful counter examples. is still a challenge, or was for us, anyway, and one of the things that's frustrating is when you know, for example, Z 3 has really almost magical ability to deal with quantifiers I thought it

00:51:39.000 --> 00:51:51.000
was incredible how well it worked, but it doesn't always work. and sometimes the the problem you get is a timeout and so trying to figure out why something is taking a long time in decision procedures.

00:51:51.000 --> 00:52:07.000
So you can figure out what you might be able to do to to fix it is very, very hard, and I think, support. Better support for that in smt solvers would be very welcome for the intervened language boogie

00:52:07.000 --> 00:52:12.000
boogie once was also for us something that enabled us to complete this project.

00:52:12.000 --> 00:52:24.000
I don't think we could have done it without it, but we did struggle a bit to present good counter examples to our users, and sometimes extracting that information from Bogey was not as easy as we hoped it would

00:52:24.000 --> 00:52:35.000
be, in fact, shares. Kadir, who had some experience with Boogie in the past and was on our team, made changes in Boogie to improve our ability to get counter examples, finally is the issue of time and

00:52:35.000 --> 00:52:49.000
patience and development of these systems i've thought about why haven't formal methods had even more impact and achieved the dreams that people had 30 or 40 years ago, and i've concluded that a lot of it

00:52:49.000 --> 00:53:02.000
is. It's just hard and I know I have ideas for how we can solve some of the longstanding problems with application of formal methods, particularly for you know straight.

00:53:02.000 --> 00:53:14.000
You know what we were trying to do in the move pro, and is trailing 10 or 20 years behind the kind of research that was described in the formal methods in the field program.

00:53:14.000 --> 00:53:26.000
But still not all the problems are solved. And yeah, the technology that we use to enable this project was developed over a period of 20 or 30 years.

00:53:26.000 --> 00:53:40.000
And so I think that some of this is just gonna take if it's ever going to be have the impact we would like He's gonna have to just take more resources and a sustained effort you know sometimes that's

00:53:40.000 --> 00:53:45.000
what's required to get over the hump with something I feel that's where we are with formal methods.

00:53:45.000 --> 00:53:51.000
It's a little difficult to justify in an industrial context, or even in a government funding context.

00:53:51.000 --> 00:53:57.000
Any experience in academia I wanted to get. This is my last slide.

00:53:57.000 --> 00:54:01.000
I wanted to give a shout out to the previous work in this area.

00:54:01.000 --> 00:54:06.000
So in itself, I think. Well, it is. have provided my first funding.

00:54:06.000 --> 00:54:10.000
When I was a junior faculty member and provided a lot of funding on on the way.

00:54:10.000 --> 00:54:18.000
Nsf. is the most visionary funding agency, and as a university professor I found to be the easiest to work with.

00:54:18.000 --> 00:54:26.000
They understood research and out, worked in universities and maximize the the productivity impact of university researchers.

00:54:26.000 --> 00:54:39.000
This. This work is is based on as i've said Decades of government funded research much of for men as F. a lot of it from Darpa, and from other sources as well.

00:54:39.000 --> 00:54:45.000
There's a huge contribution of Industrial research goes well beyond impact on the companies doing the research,

00:54:45.000 --> 00:54:50.000
Particularly Microsoft, which we use very heavily. before Microsoft.

00:54:50.000 --> 00:54:55.000
Some of the people who developed this technology we're at universities.

00:54:55.000 --> 00:55:06.000
Some of them were a decade systems research. center I guess it was in Palo Alto which we collaborated with a little bit a long, long time ago. I don't know the deck ever benefited financially from that work but the world

00:55:06.000 --> 00:55:14.000
certainly did and work at Sri International. So the benefits.

00:55:14.000 --> 00:55:22.000
Yeah, these these things benefit of the world and we're really Lucky that these companies have chosen to do this kind of work.

00:55:22.000 --> 00:55:32.000
Sri International is a government contractor, but the other ones I mentioned. I should include Amazon in this list because I know they're doing a tremendous amount of work and exporting it to the world.

00:55:32.000 --> 00:55:50.000
We didn't happen to take advantage of that in our project but I should have included it on the slide, and did not, and finally see, people on our project and on industrial projects in general are all trained and supported by or

00:55:50.000 --> 00:55:54.000
generally by government funded research, often in the United States.

00:55:54.000 --> 00:56:07.000
And you know, it would be really interesting to trace any what back from any one of these projects, and where the technology, and particularly where the people came from, and how they were trained, and how they were supported But i'm pretty confident that it would

00:56:07.000 --> 00:56:16.000
all get back to Us. Government funding agencies in many cases, although one of the key members of our team got his PHD.

00:56:16.000 --> 00:56:20.000
In Germany, where his research was funded by, I believe, the German Government

00:56:20.000 --> 00:56:34.000
So I wanted to acknowledge the explicitly acknowledge the contributions of government funded and industrial research to the effort we were trying to do, which was completely necessary to enable us to go

00:56:34.000 --> 00:56:47.000
forward. Thank you, thank you, Dan. hi, betty quick questions before being one to the next. Yep.

00:56:47.000 --> 00:56:59.000
It's again. Yeah, if you have any questions ?

00:56:59.000 --> 00:57:13.000
I'm So yeah, I guess the because actually your next I'm trying to figure out how to unscreen share.

00:57:13.000 --> 00:57:22.000
And now i've lost my window is that gonna cause a problem, or can somebody else do it for me?

00:57:22.000 --> 00:57:32.000
Do you see? Stop here somewhere

00:57:32.000 --> 00:57:45.000
This is ridiculous. i'm sorry i've lost my zoom window somebody has stopped sharing to stop cool.

00:57:45.000 --> 00:57:54.000
I pick up the icon. There we go. Okay.

00:57:54.000 --> 00:58:02.000
Okay, you guys are okay. i'm not taking over the screen anymore. yeah, Actually, you can share your screen.

00:58:02.000 --> 00:58:05.000
Yeah, Yeah. Can you hear me? Okay, And can you see my slides?

00:58:05.000 --> 00:58:18.000
Okay, this is good. Yeah. Thanks. Okay, So let me start my talk by thanking the Nsf and Raji for for this wonderful panel.

00:58:18.000 --> 00:58:24.000
And special thanks to myself in particular, because, my PHD research was funded by National Science Foundation.

00:58:24.000 --> 00:58:37.000
A large part of it via what was then the goalie program, grandpa? opportunities for academic teasers with industry and Toyota was the industry partner on that particular project.

00:58:37.000 --> 00:58:41.000
And so I really command Nsf for continuing to fund this.

00:58:41.000 --> 00:58:47.000
This line of research in this important area that bridges the gap between academia and industry.

00:58:47.000 --> 00:59:00.000
So the outline of my talk is gonna be i'll. i'll maybe take a couple of slides to put some context about verification and validation at mathworks, and then talk about the the 3 things

00:59:00.000 --> 00:59:06.000
that we have been requested to talk about, which is the success stories challenges in our future case.

00:59:06.000 --> 00:59:10.000
Okay, So those of you who may not know what math works is we are.

00:59:10.000 --> 00:59:16.000
We are 2 developers, and probably the most famous tool that comes out of networks is Matlab.

00:59:16.000 --> 00:59:25.000
It's a graphical, it's a programming language, but algorithm development, data, analysis, visualization, etc., based on linear algebra.

00:59:25.000 --> 00:59:34.000
Then there is simple languages or a platform for a block diagram modeling environment for design, simulating, analyzing and testing systems.

00:59:34.000 --> 00:59:37.000
And then there are more more than 2,120.

00:59:37.000 --> 00:59:41.000
Add-on products that build on either Matlab or civil link, or both.

00:59:41.000 --> 00:59:57.000
Like the competition toolbox here. So in terms of new number of users, we have, you know, over 5 million users in the world, basically pretty much. And we are lucky to have users both from industry in

00:59:57.000 --> 01:00:03.000
terms of, you know, aerospace and automotive shown here on the slide as well as you know.

01:00:03.000 --> 01:00:16.000
Lots of lots of users from Academia as well, and some of the trade-offs. that that sort of get discussed are have to do with You know how to bridge this this whole spectrum of people who build

01:00:16.000 --> 01:00:26.000
established products that require, you know, rigorous tools to complete their workflows as well as you know, those who are building sort of new groundbreaking and breakthrough research.

01:00:26.000 --> 01:00:42.000
Ideas. So, on the one hand, you know, there are concerns about what is even possible to solve, and, on the other hand, you know, making tooling and and and what we provide more robust and user ball, etc.

01:00:42.000 --> 01:00:51.000
So verification of valuation at mathworks has to do with basically lots of different products and and supports several different workflows.

01:00:51.000 --> 01:00:56.000
Some of them use formal methods, others are more practitioner oriented.

01:00:56.000 --> 01:01:07.000
They are more principle approaches I want to acknowledge that polypace and simulating design verifier, are a couple of products that do use formal methods, but they are not the focus of

01:01:07.000 --> 01:01:16.000
today's presentation so what I wanted to talk instead about today is a couple of recent success stories mainly on the specification side.

01:01:16.000 --> 01:01:24.000
One is specification, formalization using temporal assessments and the other one is specification modeling using deployment stable block.

01:01:24.000 --> 01:01:28.000
So let's get right into it for the specification formalization.

01:01:28.000 --> 01:01:42.000
Recently we've seen in the research community at least on the sort of embedded inside the physical system side that, using temporal logics or formalizing specifications in general helps uncover mistakes and what you see on

01:01:42.000 --> 01:01:52.000
the bottom left of the screen is an example of the kinds of mistakes that it can uncover; that one being from a a model from Toyota.

01:01:52.000 --> 01:02:07.000
Oh, at the same time. basically, this use of symbols and vocabulary for for temporal logics is really hard for for industry practitioners.

01:02:07.000 --> 01:02:12.000
And this slide comes from jordan's first slide from the Fcc.

01:02:12.000 --> 01:02:17.000
Keynote from 2,015, and this still rings true. right.

01:02:17.000 --> 01:02:26.000
So what we have done in the recent past is basically taken that approach, where, we have tried to combine the best of both worlds.

01:02:26.000 --> 01:02:35.000
Where, we allow users to specify temporal properties without really having them to specify temporal formulas.

01:02:35.000 --> 01:02:48.000
So we have developed this Ui as part of simulating test manager, which is part of simulating test which lets you kind of fill in the templates for specifications and talking with our industry.

01:02:48.000 --> 01:02:54.000
Customers, I mean most of our specifications are of the for trigger response.

01:02:54.000 --> 01:02:58.000
So there is some trigger, and eventually there is some response.

01:02:58.000 --> 01:03:11.000
Oh, right! And so you can just fill in the various components of this formula template, which is, you know, the pre condition, the temporal nature of it, of the response, and the the response itself.

01:03:11.000 --> 01:03:19.000
And then you can basically iteratively fold this expression to read it like an English language sentence.

01:03:19.000 --> 01:03:23.000
So you know this is more familiar to the practitioners it's it's familiar.

01:03:23.000 --> 01:03:36.000
It, because it, you know, reads more naturally like a English language sentence, but it's a valid logical formula, and you can use it to to test whether it it it holds and again, this is

01:03:36.000 --> 01:03:40.000
this is an example that shows a painting test result.

01:03:40.000 --> 01:03:45.000
So there is a graphical and textual explanation of the top, and at the bottom, you see.

01:03:45.000 --> 01:03:51.000
You can zoom in temporarily as well as i'm porting the expression tree to uncover where the mistakes are.

01:03:51.000 --> 01:04:07.000
And so one thing i'd like to highlight here is the sort of 3 3 level answer shown on the top of the blocks here one that shows fail pass and untested, and that's because for for

01:04:07.000 --> 01:04:18.000
practitioners. when the precondition is false, then the formula evaluating vectors due to true, you know, does not mean sense.

01:04:18.000 --> 01:04:20.000
So we had to basically show it, you know, does not make sense. So we had to basically show it.

01:04:20.000 --> 01:04:26.000
As satisfied only when the pre-condition is satisfied and the rest of the time is is kind of shown as untested.

01:04:26.000 --> 01:04:35.000
So those are some of the trade-offs that go behind the scenes in terms of introducing these to the to the community, and more for more details.

01:04:35.000 --> 01:04:41.000
I would refer to our tool paper that came out in runtime education compounds of last year.

01:04:41.000 --> 01:04:50.000
So. let me move on to the second success story, which is about specification modeling, using requirement, stable block and the workflow.

01:04:50.000 --> 01:04:57.000
There is that you want to verify the requirements themselves before you have put together the design model.

01:04:57.000 --> 01:05:10.000
So really making it early into the design design cycle. And the stable talk is basically a sequence of rows which had each have a precondition and a post condition.

01:05:10.000 --> 01:05:25.000
And it basically says, If condition is true, then requirement, that the output conditions through our post-condition store and optionally has some duration which means that you know the the input condition works for 10 s And So

01:05:25.000 --> 01:05:30.000
The benefit like, I said, is that we can really do this before even the design model is built.

01:05:30.000 --> 01:05:35.000
And we can analyze this set of requirements together.

01:05:35.000 --> 01:05:41.000
To to check for things like. Are these requirements consistent with each other?

01:05:41.000 --> 01:05:47.000
So what that problem turns out to be is basically a Smt problem.

01:05:47.000 --> 01:05:52.000
So consistency is basically can these requirements be satisfied together?

01:05:52.000 --> 01:05:57.000
And the negation of that is basically is there a setup input combination.

01:05:57.000 --> 01:06:03.000
It's a combination of inputs for which no matter what combination you choose.

01:06:03.000 --> 01:06:09.000
You can always find a you know a way that the requirements are are false.

01:06:09.000 --> 01:06:16.000
So there is no design that you can Come up with that'll make them true for that set of inputs right.

01:06:16.000 --> 01:06:28.000
So that's a pretty strong check that We can do. And we can turn this into an smt query. and then if that smt query is unsatisfiable, then the answer is the table is okay, because the negation

01:06:28.000 --> 01:06:37.000
is unsatisfiable. and if the negation is satisfied, then you know, that becomes a counter example for the for the analysis.

01:06:37.000 --> 01:06:41.000
And we use actually z 3 for this smt solving.

01:06:41.000 --> 01:06:46.000
And here is a account for example, how it's shown to the user.

01:06:46.000 --> 01:06:49.000
Basically, things that are inconsistent or highlighted.

01:06:49.000 --> 01:07:07.000
And in this example the inconsistency is that, under a normal operating condition and under an emergency subdivision something that checks the locking variable to it basically requires them to be both locked and

01:07:07.000 --> 01:07:13.000
unlocked at the same time. So this is not possible, no matter what kind of design.

01:07:13.000 --> 01:07:17.000
You come up with right so so that's the example of the kinds of checks.

01:07:17.000 --> 01:07:20.000
This can do. There is also a completeness check that this table can do.

01:07:20.000 --> 01:07:25.000
But i'll not go into that today. the other workflow is when you have a design model.

01:07:25.000 --> 01:07:35.000
How do we check sort of that? This particular design model satisfies the the requirements the earlier was like any possible design model, right?

01:07:35.000 --> 01:07:40.000
And now we are talking about this particular one, so that one is a model setting problem.

01:07:40.000 --> 01:07:49.000
And then we send this out to simulating design verifier, which can formally correct a formally basically find a counter example.

01:07:49.000 --> 01:07:56.000
Whether for this particular model, you find that these requirements are not satisfied.

01:07:56.000 --> 01:08:11.000
And an example is shown here where a couple of rows are shown together, and then there is a hyperlink to the counter example that you can use to debug either your design models or your requirements

01:08:11.000 --> 01:08:16.000
themselves. So with that, let me briefly talk about now.

01:08:16.000 --> 01:08:19.000
Some challenges based on what I have seen.

01:08:19.000 --> 01:08:23.000
And then move on to opportunities. And I chose this order because I want to.

01:08:23.000 --> 01:08:28.000
You know, finish on, and you know, positive note of opportunities.

01:08:28.000 --> 01:08:32.000
So challenges remain. in terms of system, complexity, basically.

01:08:32.000 --> 01:08:36.000
So this heterogeneity of modern formalism was a topic of my PHD.

01:08:36.000 --> 01:08:46.000
Thesis, and this it's still a bit of an unsolved problem, I would say, and to to you know, make it more interesting and challenging.

01:08:46.000 --> 01:08:59.000
There is more learning elements that are into the mix which is making analysis even more difficult to to basically reason about the correctness of the underlying system.

01:08:59.000 --> 01:09:07.000
When elements of the model are across, you know different kinds of formalisms, and they make interdependent assumptions on each other.

01:09:07.000 --> 01:09:11.000
Right. So there are some still challenges about solving this problem.

01:09:11.000 --> 01:09:17.000
To add to the mix with the advent of intimate of things and industrial Internet.

01:09:17.000 --> 01:09:31.000
And all these paradigms you don't know where exactly the model is some elements might live on an edge device next to and an embedded physical asset.

01:09:31.000 --> 01:09:34.000
Some might live in the cloud etc. Right?

01:09:34.000 --> 01:09:37.000
So how do we put together something that is compositional?

01:09:37.000 --> 01:09:45.000
And works across different platforms and and and infrastructure where the the model elements live.

01:09:45.000 --> 01:09:58.000
And last, maybe you've seen recently that the model based design approach, where models you know, are used for at the design phase is now increasingly turning into a model based operations where models are still used in operation

01:09:58.000 --> 01:10:04.000
and you've seen this sort of devops workflow of, you know, continuous integration and continuous deployment.

01:10:04.000 --> 01:10:09.000
That makes the questions about. Can we do sort of incremental verification?

01:10:09.000 --> 01:10:15.000
David, touched about it a little bit. but there are, you know, problems to be solved here about.

01:10:15.000 --> 01:10:33.000
You know, What can we do about you know making sure that earlier analysis still hold and and things like that. for the opportunities let me maybe focus on ai enable engineering systems which is the recent trend where people are

01:10:33.000 --> 01:10:38.000
using Ai enabled blocks into in engineered systems.

01:10:38.000 --> 01:10:51.000
So as part of symbolic, we have introduced, you know, blocks that have Ai elements into them, from either statistics and machine learning approaches, or some neural network approaches or reinforcement

01:10:51.000 --> 01:11:06.000
learning as well as just you know embedded C code, which is which would be say using computer vision kind of algorithms right where you can exercise, you can use them to exercise them as if it's like any

01:11:06.000 --> 01:11:11.000
other symboling blog to to make sure that your analysis is working.

01:11:11.000 --> 01:11:31.000
Okay, and it's buck free right but the challenge Here is that specifications, especially for more specifications is, still a hard problem. and people are mostly doing sort of robustness style of analysis on these neural networks where If you port up the

01:11:31.000 --> 01:11:38.000
system a little bit can you, guarantee something about the output of the network?

01:11:38.000 --> 01:11:41.000
So in that period. this is very recent work.

01:11:41.000 --> 01:11:47.000
So this has come out as a support package maybe one or 2 weeks ago. it's called a deep learning tool.

01:11:47.000 --> 01:12:00.000
What's verification library and it's based on this work out of eth zoom that came out in purple of 2,019 and the kinds of things that this can do is you know

01:12:00.000 --> 01:12:04.000
given a network and some limits on my input participation.

01:12:04.000 --> 01:12:08.000
What is my output? perturbation, etc.?

01:12:08.000 --> 01:12:15.000
And I just want to acknowledge that there are other people, maybe, in on this call who are working on this.

01:12:15.000 --> 01:12:18.000
Raji is a very sick and taylor Johnson's N.

01:12:18.000 --> 01:12:33.000
Andb are a couple of examples that come to mind i'm Sure, there are a lot more. then, in this similar spirit there is another line of work that we have recently open source which is called neuron coverage

01:12:33.000 --> 01:12:40.000
for deployment. And the idea here is to use coverage metrics that are used for code coverage.

01:12:40.000 --> 01:12:50.000
To basically, you know, see whether whether it can provide any sort of analysis benefit to the users as well.

01:12:50.000 --> 01:13:04.000
We It remains to me it's still only days and It remains to be seen whether this is a useful metric for sort of robustness, and and, you know all these properties of off the underlying system, performance.

01:13:04.000 --> 01:13:13.000
if you were to do coverage sort of analysis on the network it's It's not it's not clear yet.

01:13:13.000 --> 01:13:18.000
Oh, and so this is some examples that blocks about this.

01:13:18.000 --> 01:13:24.000
And Let me mention one more block, which is the constraint enforcement block.

01:13:24.000 --> 01:13:31.000
This is sort of based on the control barrier function, and etc., like a line of research from the controls community, right?

01:13:31.000 --> 01:13:40.000
And what it's doing is basically adding a layer of safety enforcement for reinforcement learning algorithms.

01:13:40.000 --> 01:13:56.000
But you could also use it for traditional control design. And the idea is basically whenever you get an answer that is, that does not satisfy a a constraint that you would like it to satisfy you solve a optimization problem

01:13:56.000 --> 01:14:03.000
that gives you the nearest value that does satisfy the enforcement, so that you don't learn any unsafe variables.

01:14:03.000 --> 01:14:14.000
Whatever you've done is is safe so this is again, The formal methods adjacent line of work, I would say so.

01:14:14.000 --> 01:14:20.000
With that, I mean that's the so when my that is the you know end of my talk.

01:14:20.000 --> 01:14:34.000
I would like to summarize that, you know. we have seen recent success stories of formal methods being turned into sort of practice without burdening the users challenges still remain about you know complexity, of

01:14:34.000 --> 01:14:40.000
the system. So so, that's what motivates us and lots of future opportunities.

01:14:40.000 --> 01:14:52.000
We see in this in this area of Ai enable systems where domain specific, you know, standards and best practices are beginning to emerge across sort of embedded medical devices abr next automotive.

01:14:52.000 --> 01:15:01.000
And so on. So with that I'd like to conclude my talk and hand it back to Rajiv.

01:15:01.000 --> 01:15:04.000
Thank you. So there are a couple of questions.

01:15:04.000 --> 01:15:20.000
So my name's from and you thoughts and applications on the that the component don't shared a global clock

01:15:20.000 --> 01:15:30.000
Well, we're working I i'm thinking about it but I think it's a little bit more advanced, I think, at the practitioner levels like immediately.

01:15:30.000 --> 01:15:42.000
We don't have much to say that Okay, and There is a question from Steve Segal the work on temporary formula offering reminded me of academic work.

01:15:42.000 --> 01:16:06.000
Front 22,000 by the propell property, and which was a nice tool for editing temporal properties and viewing them in different languages, including English offices in Lpa, just wondering if this work influence the work of

01:16:06.000 --> 01:16:20.000
networks I wouldn't say directly. influenced I would I would say, we work with our industry sort of customers in terms of what would it make sense to them?

01:16:20.000 --> 01:16:25.000
So at the specification time I mean there I didn't get time to go into all the details.

01:16:25.000 --> 01:16:33.000
But there's probably some screenshots in the paper that show like at edit time, when the signal the actual behavior is not available.

01:16:33.000 --> 01:16:44.000
You know what kinds of sample cartoon behaviors we should show to evoke the kinds of things that they should be thinking about while writing the property in a particular way, etc.

01:16:44.000 --> 01:16:47.000
And then, when you show this why are you? Why right?

01:16:47.000 --> 01:16:57.000
So there is also also a trade-off about expressivity versus what will become like for cumbersome in terms of, you know, specifying wire a ui, etc.

01:16:57.000 --> 01:17:05.000
So those kind of when some of those decisions went into, you know, implementing the way that we have.

01:17:05.000 --> 01:17:21.000
Okay, thanks. So let's let's move on can share your screen and

01:17:21.000 --> 01:17:26.000
I think this thing my browser needs to give access to.

01:17:26.000 --> 01:17:33.000
Given that i'm gonna have to quit and reopen because my browser does have to quit and reopen, I'll be back in a second.

01:17:33.000 --> 01:17:38.000
Okay, So Oxford is another question for you from Osama Bass.

01:17:38.000 --> 01:17:45.000
So on the team of making the Tc. to create from formal specifications. do customers benefit?

01:17:45.000 --> 01:17:56.000
Are asked for automatic learning of specifications from the crisis generated by legacy designs

01:17:56.000 --> 01:18:04.000
So I guess specification mining is that, like a good research direction from the traces from data?

01:18:04.000 --> 01:18:16.000
Oh, maybe i'm i'm not sure we we've kind of heard it in the in the context of you know, managing experiments, and so on.

01:18:16.000 --> 01:18:24.000
But not specifically. You know, mining specifications. One of the challenges is because, you know, models get developed for different purposes.

01:18:24.000 --> 01:18:33.000
Right. So with different purposes in mind. So if not done via formal specification.

01:18:33.000 --> 01:18:43.000
Manager. it's not clear whether you know we should be using the results from another model for a different context.

01:18:43.000 --> 01:18:58.000
Okay, Thanks. yeah. i'm back But it's somehow not letting me share this screen for some bizarre reason the who dns that?

01:18:58.000 --> 01:19:05.000
I guess the it folks that's I guess she is they have a badness to that.

01:19:05.000 --> 01:19:10.000
She have permission to share

01:19:10.000 --> 01:19:21.000
Yeah, I think Chief, she does do you want to send send me, or Nina, your your Yeah, it's gonna be hard.

01:19:21.000 --> 01:19:22.000
Just let me let me try one quick thing i'll be back again.

01:19:22.000 --> 01:19:42.000
Just one more minute. She just became co-host, so maybe no, she can

01:19:42.000 --> 01:19:49.000
Okay, meet by anyone. If you have any questions for actually or Dave or Nicolai, it's, you know.

01:19:49.000 --> 01:19:54.000
Yeah, we have

01:19:54.000 --> 01:20:13.000
We have. we have had, you know, give you a diversity of application, the units could be used, so that That's great

01:20:13.000 --> 01:20:22.000
I think the the computer is not allowing the recording. I actually think that might be the problem.

01:20:22.000 --> 01:20:30.000
Yeah, You can email anyone up as you like me or be your slides.

01:20:30.000 --> 01:20:41.000
That would be please

01:20:41.000 --> 01:20:45.000
I just sent you a request. if you want to send them to me.

01:20:45.000 --> 01:20:48.000
I left you my email in the chat, and I can display them for you.

01:20:48.000 --> 01:20:56.000
Okay, because i'm doing what it says here and i'll be able to

01:20:56.000 --> 01:21:02.000
So actually, I don't pay maybe maybe have the whatever it was like.

01:21:02.000 --> 01:21:07.000
Next go first, and then i'll by the time i'll send slides to Yeah.

01:21:07.000 --> 01:21:14.000
So I saw some movie, maybe. Why, don't you go ahead and fine.

01:21:14.000 --> 01:21:26.000
Yeah, hi, everybody. I also wanna is that slide. I think it should be easy.

01:21:26.000 --> 01:21:29.000
Can you see my slides? Yes, we can see your screen.

01:21:29.000 --> 01:21:34.000
Yeah, okay. So first of all, I also want that acknowledge.

01:21:34.000 --> 01:21:43.000
And I said, especially I was working extensively in my career with Tom Max, and generous support for Minnesota.

01:21:43.000 --> 01:21:48.000
Many of the people in my team actually are graduate from medicine.

01:21:48.000 --> 01:21:59.000
And the talk that i'm gonna talk today. is our startups which we started Actually, we'll we'll be celebrating 4 years in the in actually a few days.

01:21:59.000 --> 01:22:04.000
And this is actually taking the techniques of formal method.

01:22:04.000 --> 01:22:15.000
Specifically smd and static analysis, and putting them actually to find huge bugs in the area of smart contract.

01:22:15.000 --> 01:22:33.000
So our team actually is up grow quite quickly. We have about 90 people in the team, many of them actually have Phds from, I said, and they actually we have you fantastic group in the Us.

01:22:33.000 --> 01:22:40.000
And also fantastic group in Europe, supported by upn and also fantastic group in in Israel.

01:22:40.000 --> 01:22:46.000
The old domain expert in the of smt and static analysis. and we need them.

01:22:46.000 --> 01:22:50.000
Actually the problem that we are solving are very hard, and we need them.

01:22:50.000 --> 01:23:05.000
We feel that we need to push the R and D to make these techniques work, and we actually contributing already to static and as an smt in order to solve the problem which are raised by our customers, we also have actually

01:23:05.000 --> 01:23:12.000
fantastic people that we are hiring which are not actually domain expert in the area study guys in S and T.

01:23:12.000 --> 01:23:21.000
But they are domain expert in code security. In particular, I wanna come back, I mean, Levy was actually used to be head of the security in the idea.

01:23:21.000 --> 01:23:27.000
So these are people actually helping our customer with with actually writing the specification.

01:23:27.000 --> 01:23:37.000
And actually using this technology, this is equally important. This technology is actually used now and actually, but our software is not open source.

01:23:37.000 --> 01:23:43.000
But you can. If you want, you can access the software from our website, there's a free version.

01:23:43.000 --> 01:23:53.000
You can use it to check called at the moment it's working solidly, but coming back is coming next is right there, and then vast, and then move.

01:23:53.000 --> 01:23:56.000
All of them are actually being checked so it's related to David, Stop!

01:23:56.000 --> 01:24:04.000
We have this technique, and It's under the boot of course it calls tools like Yeah, Z 3 Cbc. 5.

01:24:04.000 --> 01:24:16.000
It's actually combined, and simply sold by queues A lot of smt solving under the hood the pain point that we are addressed is actually has nothing to do with each other.

01:24:16.000 --> 01:24:22.000
It's a pain point that everybody is worried about is basically exploitable software.

01:24:22.000 --> 01:24:34.000
But in the area of smart contents, actually very interesting, because you have a small code which is manipulating a lot of money, and you can make mistakes which actually will cost you 1 billion dollars.

01:24:34.000 --> 01:24:38.000
And actually they were already found by a tool. Also, the code is immutable.

01:24:38.000 --> 01:24:44.000
So once the code is deployed it's hard to change and the concept here is called as low.

01:24:44.000 --> 01:24:53.000
So if you have a wrong call, it's a long long the other part that we are addressing is the problem is sort of how do people actually?

01:24:53.000 --> 01:24:58.000
And this is, how do people check the code in the air of smart contract?

01:24:58.000 --> 01:25:02.000
The standard that is influenced usually by Vcs.

01:25:02.000 --> 01:25:10.000
And other is what's called manual auditing so man you already think these are people security with security, minds that you are reading your call.

01:25:10.000 --> 01:25:20.000
Some of them do fantastic job. but still it's very very hard to find these people, and also these people we are finding even box after them.

01:25:20.000 --> 01:25:24.000
The other problem which we are twice is the ineffectiveness of tools.

01:25:24.000 --> 01:25:29.000
Basically tools fail and tool can fail by false, positive force, negative.

01:25:29.000 --> 01:25:35.000
And also the very hard to use, and how the tool we are pushing very hard to make it easier to use.

01:25:35.000 --> 01:25:43.000
We have still far. I think we have to make it much easier to use in the in the next.

01:25:43.000 --> 01:25:50.000
In this talk you have to talk about box, and actually done a lot of box.

01:25:50.000 --> 01:26:00.000
But this year there have been many, many fantastic box. The bug is I, and many of these, and these are the ones here. some time, of course not.

01:26:00.000 --> 01:26:06.000
Coding arrows, but these are all called cordials, and they are all logical errors.

01:26:06.000 --> 01:26:10.000
So these are mistakes in the code that were exploited to still demise.

01:26:10.000 --> 01:26:18.000
So the Norman bridge is a very very interesting example it's a case that somebody update the code to change the very recent.

01:26:18.000 --> 01:26:27.000
But and basically the heck actually was a nice guy. He just told a little money. but then people after him, they saw it, and they stole the best.

01:26:27.000 --> 01:26:35.000
So basically, what happens is actually a very recent thing. Compound is a very interesting case, because they actually do work with Saturday.

01:26:35.000 --> 01:26:43.000
But what happened? People who built on top of them didn't use our technology, and as a result they lost their 18 million dollars.

01:26:43.000 --> 01:26:54.000
So basically, and we are actually working now together, making this tool available, not just to developers, but also to people who built on top of the development.

01:26:54.000 --> 01:27:09.000
So we are making this tool available now to to more people so that they can check the code. and it's of course, related to David to talk about using the technology in in part of Ci as part of continuous integration.

01:27:09.000 --> 01:27:14.000
How does our tool work? It work exactly as you expect, Like you.

01:27:14.000 --> 01:27:19.000
You write your environment, and then you write your code. It could be installed.

01:27:19.000 --> 01:27:26.000
It can be another language. And then we have this prover, and this prover can either tell you that the environment is full.

01:27:26.000 --> 01:27:32.000
But the more interesting cases it can give your back. and this can be a potentially whereabout.

01:27:32.000 --> 01:27:37.000
And this is how we work. We provide the invite to our customer working environment.

01:27:37.000 --> 01:27:47.000
And basically they use this technology to check and this is a technology that the moment is it's running on the cloud Austin aws.

01:27:47.000 --> 01:27:51.000
There is a very powerful machine, and under the whole it's one smt soldo.

01:27:51.000 --> 01:27:55.000
Actually it combined many ascent tools as simply solve them together.

01:27:55.000 --> 01:28:05.000
To solve this problem. Of course we know in this domain, and this is our enemy is that we have time out of the Smt.

01:28:05.000 --> 01:28:11.000
And our our smt formulas are very complex. So, in fact, there are a lot of failures of the tool.

01:28:11.000 --> 01:28:16.000
We are working on them, together with a lot of support from N.

01:28:16.000 --> 01:28:29.000
Equalized Z 3 Cbc. 5 team, everybody who can help us, And we have to get as many hope as we can to to basically show these Smt phone ones.

01:28:29.000 --> 01:28:38.000
The the other use case. And this is what imagine in in David Deals talk is that we integrated in part of the Ci.

01:28:38.000 --> 01:28:42.000
And many of our customers. They integrate this in part of the development pipeline.

01:28:42.000 --> 01:28:51.000
So basically every time they change the call, assuming that the advance remains the same, they run the tool again and again and again.

01:28:51.000 --> 01:28:55.000
Notice in our domain. I like tools like Daphne. we only write the invalion.

01:28:55.000 --> 01:29:02.000
So this means that there is actually more complex score for the technology to hand.

01:29:02.000 --> 01:29:14.000
So basically, every time you you, you change the code, you want this technology in order to prove options of bug or find new bugs.

01:29:14.000 --> 01:29:22.000
Okay, I think, David ended with the complicated problem. So I wanna start with the complicated problem.

01:29:22.000 --> 01:29:31.000
So Smt solver it's a huge success but in our experience. There's a lot of things that need to be improved to make them useful in our domain.

01:29:31.000 --> 01:29:43.000
So we are talking about financial systems. so no lady i'm mathematics is very heavy used there, and in fact, our tool phase a lot in nonlinear.

01:29:43.000 --> 01:29:50.000
We have our own solution, but the, I think many more are needed also in crypto currency.

01:29:50.000 --> 01:30:01.000
The number of so very big, so if you're trying to Use something like big vectors, So that's basically very, very hard, because you have 202 2 or 56 meet integers.

01:30:01.000 --> 01:30:13.000
It's very, very, hard hard to scale it and another problem that we see is that the usage we and we are handling low level code. And but it's also the case for high-level code that if you want to go

01:30:13.000 --> 01:30:19.000
using a rate theory. It doesn't scale we have our own methods, and we rely on static and early.

01:30:19.000 --> 01:30:27.000
But still it it has to be improved I don't think that we worry about this quantification because we want to make the environment useable.

01:30:27.000 --> 01:30:33.000
We don't want to use quantifies and and If you are what have quantify, especially quantified donation.

01:30:33.000 --> 01:30:40.000
This is where Smt Solver do not work for us for us. since we work in financial system.

01:30:40.000 --> 01:30:49.000
Also we need high order visiting in particular, you need something like summation, and this is, of course, something which is hard for the Sd.

01:30:49.000 --> 01:31:01.000
I also want to point out, and maybe this is august in this community that even if you have something working in a single turkey once you combine to you, it's very, very high and in another August probably is size, what was

01:31:01.000 --> 01:31:11.000
you formula, and it's very very very hard for smt to scale to these new formula we do have some kind of reliability that we are doing for a reason.

01:31:11.000 --> 01:31:26.000
But still it's very, very, for hard for us to scale So the lot of research to be done to make this technology more broadcast, and we we have to tell you we have the white paper and we have to share with have papers describing some

01:31:26.000 --> 01:31:35.000
of the academic wealth. But we love to get as many help as we can to solve this problem.

01:31:35.000 --> 01:31:42.000
How is this tool working? So this is a basically the the way the tool works?

01:31:42.000 --> 01:31:47.000
It's actually takes the solidity call and then it goes to the Evm.

01:31:47.000 --> 01:31:55.000
Ebm is a by code of detail, and then we have our own decompile, something which is actually go back to the work of Floyd handling.

01:31:55.000 --> 01:32:02.000
And the University of Mcgee. Basically, you can find bounds on the stack and get some symbolic presentation.

01:32:02.000 --> 01:32:07.000
We call it that we have this call, and then we combine the invite also to talk.

01:32:07.000 --> 01:32:14.000
And then we have the verification condition, where we do a lot of things in order to get an smt formula.

01:32:14.000 --> 01:32:28.000
And then there isn't 2 phone lines is fed to a one seldom or many sober in order to either find a bag or prove an absence of that interesting thing that we found out that actually is, it's a game change

01:32:28.000 --> 01:32:31.000
of wise, especially because we let work on low level code.

01:32:31.000 --> 01:32:36.000
Do we need to specialize the code, And we actually do a lot of static analysis.

01:32:36.000 --> 01:32:41.000
But the users of static analysis in order to simplify the code.

01:32:41.000 --> 01:32:46.000
So this we are doing something which is, you can call it a cheat.

01:32:46.000 --> 01:32:50.000
What we do is actually, we enforce certain stronger environment on the code.

01:32:50.000 --> 01:32:56.000
And we change this invite. we call it trust and verify and there we're using opposite interpretation.

01:32:56.000 --> 01:33:05.000
This is actually where we can recover storage. We can recall a high high level type, and we are doing it without restricting the program.

01:33:05.000 --> 01:33:12.000
So basically we are taking 2 into account, some kind of assumptions on the compiler itself, and we are doing it for solidity.

01:33:12.000 --> 01:33:20.000
We are doing it for us. The interesting thing about this thing is that it actually give us a lot of bug in the compiler itself.

01:33:20.000 --> 01:33:29.000
And you can read out, basically, we find box that the compiler itself, unintentionally both this environment, because they were back in the compiler itself.

01:33:29.000 --> 01:33:37.000
So we are finding these bugs automatically with the user static analysis of object interpretation.

01:33:37.000 --> 01:33:40.000
The other things that we are doing in I won't be able to explain here.

01:33:40.000 --> 01:33:53.000
But a lot of expert in the team. specifically also a very basically show you all kind of techniques how to solve the basically to avoid the the, the, the Np.

01:33:53.000 --> 01:33:57.000
Complete, or the the understandable problem of solving smt.

01:33:57.000 --> 01:34:09.000
And of course we need to probably learn more. The community has a lot of metals, and maybe we need to learn more in order to actually make smt solving more tractable.

01:34:09.000 --> 01:34:19.000
I wanna actually use the rest, of the talk to actually show you the good things that there's and the thing that they'll send the good thing with the smt.

01:34:19.000 --> 01:34:26.000
And you guys have done for us. Actually, these are the cases that we found many, many interesting bucks.

01:34:26.000 --> 01:34:30.000
And the most interesting, probably bugs is a solvent issue.

01:34:30.000 --> 01:34:35.000
So what does the solvency mean? Solving c. you can define it formally in temporary logic?

01:34:35.000 --> 01:34:41.000
But I'm defining here. it in informally basically if everybody wants to the bank.

01:34:41.000 --> 01:34:47.000
The bank is still and this is sort of an interesting property that you want to inform.

01:34:47.000 --> 01:34:59.000
We don't write this property. we write it actually a stronger inf environment which implies this property, and here you find bugs that found by the Smt.

01:34:59.000 --> 01:35:02.000
And all of these they were found before the call was deployed.

01:35:02.000 --> 01:35:08.000
They were fine after the call was carefully audited by the best teams.

01:35:08.000 --> 01:35:13.000
And here you see the box that we found, and you see the amount of money which is safe.

01:35:13.000 --> 01:35:26.000
Okay, So this is sushi. swap for example this driving is the case that the smt find this bug. we allow you to completely drink during the money. I don't know if you know it's one of the biggest one

01:35:26.000 --> 01:35:31.000
compound. So these are bugs that are found by our tool.

01:35:31.000 --> 01:35:40.000
We will divide in this case. So the subtraction, we will the environment, and then we use them with the smt to solve.

01:35:40.000 --> 01:35:44.000
To find a box. So this is a case that bugs will find by the smt.

01:35:44.000 --> 01:35:50.000
But this is to our team. Actually we will be invited for them.

01:35:50.000 --> 01:35:53.000
The other thing, which is even more interesting. And this is actually something.

01:35:53.000 --> 01:36:01.000
I know that a lot of people say bad things about cryptocurrency, but in cryptocurrency the lot of very good people.

01:36:01.000 --> 01:36:09.000
And one of the things that we are finding out that some of our customers they know how to use our tool better than us, and without.

01:36:09.000 --> 01:36:11.000
So basically, for example, this is make here I don't know if you know.

01:36:11.000 --> 01:36:20.000
Make your doubt it's actually it's called it's actually holding about 15% of the cryptocurrency in the world, and they use the tool.

01:36:20.000 --> 01:36:26.000
You see it's basically the the the code implement something which is called a stable coin.

01:36:26.000 --> 01:36:34.000
So they statement. They they launch this code in 2,018, and they run the tool actually. did you see it?

01:36:34.000 --> 01:36:44.000
And the tool actually there's something found the back that allow you to actually break the the the basic advantage of the system.

01:36:44.000 --> 01:36:48.000
So this is about 10 billion, which were at least, and actually this.

01:36:48.000 --> 01:36:56.000
The environment was written by cool. is that If you actually wrote this environment, And actually it's very interesting.

01:36:56.000 --> 01:37:01.000
It was surprising, basically, what happened. The tool found that the basic environment is not in that.

01:37:01.000 --> 01:37:05.000
And it was found by Smt. So thank you, Nikola.

01:37:05.000 --> 01:37:09.000
It was fine by the Smt solder after the cool world.

01:37:09.000 --> 01:37:17.000
The environment. And I think that actually very interesting, that another customer.

01:37:17.000 --> 01:37:31.000
So this is another customer called 2 5, they're all the own environment. and then they did something which I don't know if you think it's fair or not, they actually call it auditing thing, and they ask them to check.

01:37:31.000 --> 01:37:41.000
The box, and they basically insert manually box, And they ask the smt solver to find the pack, and also the the the auditing team to find about.

01:37:41.000 --> 01:37:46.000
And what you see, actually that the auditors which are human they missed actually many.

01:37:46.000 --> 01:37:54.000
But okay, and and basically, you see that the formal verification is found.

01:37:54.000 --> 01:38:00.000
The more the most significant number of bugs. You see, also, the formal verification missed on that.

01:38:00.000 --> 01:38:06.000
Actually, I think, one or 2. and this is, of course, due to the inappropriate environment.

01:38:06.000 --> 01:38:20.000
We have already few customers. we just use our tool and actually they don't have the right environment that's a problem. And we are actually implementing now open source technology, which is mutation testing led by Chanda Nadi also

01:38:20.000 --> 01:38:25.000
actually supported by Nsf: So we have tools that are checking the device.

01:38:25.000 --> 01:38:31.000
Are not vacuums. they have their caring support.

01:38:31.000 --> 01:38:41.000
And what? So that's what we are doing in terms of what we are. Now, I think that this technology is actually used by the top players.

01:38:41.000 --> 01:38:53.000
I think about 50% of them. They actually use this to secure the code this is running actually on the lot of programs, And it's actually integrated into Ci.

01:38:53.000 --> 01:38:59.000
We have particularly healthy of the box that we found before the call deploy.

01:38:59.000 --> 01:39:06.000
We actually can run the 2 after the code deploy, because we are running on the X one executable, and we have found you of them.

01:39:06.000 --> 01:39:15.000
But we have specifically happy about the box that were found by these technology before the call was declared.

01:39:15.000 --> 01:39:22.000
Holy thinking about standardizing it so that's actually a huge effort for us.

01:39:22.000 --> 01:39:25.000
It bolts in the Ivan D, but also in the adoption.

01:39:25.000 --> 01:39:30.000
So we used to. Basically, this is a software service that we send to our customer.

01:39:30.000 --> 01:39:36.000
But we are trying to make this more usable, and one of the the problems of making it user.

01:39:36.000 --> 01:39:42.000
But of course, making the tool better, but also making the task of writing invariant easier.

01:39:42.000 --> 01:39:46.000
And this is where we are at the moment trying to use community.

01:39:46.000 --> 01:39:55.000
So we have now and of course, it's not as the community it's a quadrina is a community which is actually in the Us.

01:39:55.000 --> 01:40:00.000
So actually encouraging people to review, call, and what we are doing now.

01:40:00.000 --> 01:40:11.000
We are partnering with them that people when they view the call, the lighting value, and for for the call, and then they would use the tool, and from there and back bounty.

01:40:11.000 --> 01:40:18.000
So these are mechanism that encourage community to write specification and from down.

01:40:18.000 --> 01:40:25.000
We are going to what's called down which we already started is basically I already mentioned that not just the the people who write the code.

01:40:25.000 --> 01:40:29.000
Also the people who build on top of it. they they actually use it.

01:40:29.000 --> 01:40:32.000
And for that they are basically we have the people in the down.

01:40:32.000 --> 01:40:38.000
They have to vote for them. The people on the down have to vote for the adoption of the formal method.

01:40:38.000 --> 01:40:51.000
We have done the first one if we completed it. I think yesterday, and all the proposal actually got the now the highest number of to people. It means that people really like formal verification in this case.

01:40:51.000 --> 01:40:54.000
You can read about it. Look at the other proposal.

01:40:54.000 --> 01:41:01.000
People really like usage of formal verification here to make the code more secure.

01:41:01.000 --> 01:41:24.000
That's just my presentation. Thanks thank you thank you mode any in any questions for I mean, this is like a great application. last couple of years.

01:41:24.000 --> 01:41:46.000
And they have okay Now I'm gonna try once again

01:41:46.000 --> 01:41:55.000
Yeah, it's not somehow I think it's the recording part that probably so. Karen, maybe you can.

01:41:55.000 --> 01:42:01.000
You have slide, so maybe you can share them

01:42:01.000 --> 01:42:21.000
I think Karen will have to do the driving

01:42:21.000 --> 01:42:36.000
I'm Karen and Edgar are you guys gonna share the slides

01:42:36.000 --> 01:42:39.000
Karen did say that she got the slides.

01:42:39.000 --> 01:42:56.000
I got it. Okay.

01:42:56.000 --> 01:43:01.000
Okay, great softer we finally get there. so thank you for inviting me.

01:43:01.000 --> 01:43:17.000
I'm very glad to be presenting all the work and and learning about all the work that's been done, that there are great success stories for foreign methods across industry and an opportunity to present how formal methods is transforming development

01:43:17.000 --> 01:43:25.000
both inside Amazon as well as externally. next the the driving factor

01:43:25.000 --> 01:43:35.000
Here has been security, and as earlier it came up like, how do we ensure security, durability, availability, and correctness?

01:43:35.000 --> 01:43:39.000
So in the early days when folks were like, Hey, I have my workloads, my sensitive data.

01:43:39.000 --> 01:43:45.000
All on my on my on-prem systems but as i've put them on the cloud.

01:43:45.000 --> 01:43:58.000
But I have to go access them over the Internet security. becomes a key part, and that's been one of the driving factors that has led to this growth of automated reasoning across Amazon.

01:43:58.000 --> 01:44:07.000
So there's a whole website around approval security next there's also a a whole science page dedicated to all the publications.

01:44:07.000 --> 01:44:22.000
The blog post. The talks across various different groups. so the the way automated reasoning works at Amazon is it's actually distributed there isn't a separation between this is a science organization versus engineering and product each of

01:44:22.000 --> 01:44:32.000
the different automated reasoning folks are distributed and are close to the businesses themselves, so they're embedded in the engineering and service teams.

01:44:32.000 --> 01:44:40.000
So how are we applying automated reasoning i'll give a quick overview next, and it it starts with foundational Co.

01:44:40.000 --> 01:44:45.000
Next and the foundational code really is there's numerous foundational systems.

01:44:45.000 --> 01:44:57.000
You have custom, hypervisors, encryption, code, bootloaders and iot operating systems, and we are leveraging formal methods to prove the correctness of foundational low-level c systems.

01:44:57.000 --> 01:45:06.000
And use them to do automated test case generation where we validate that it actually, satisfies certain criteria.

01:45:06.000 --> 01:45:20.000
And we're we're, doing some tests but we're also using like proofs of memory safety to ensure that the code is both secure and correct, and the proof is around memory safety infinite loops and

01:45:20.000 --> 01:45:35.000
other defined loops. next. So one success story is free. our toss, which is an open source, real-time operating system for microcontrollers that essentially makes small low power edge. devices that are easy to program deployed

01:45:35.000 --> 01:45:52.000
secure, connect, and manage. and last year one version of this was downloaded every 170 s next, and we have proofs of memory, safety, thread, safety, and functional correctness of the correct queue implementation, and

01:45:52.000 --> 01:46:07.000
free artists. where there's also provides high level of assurance that the free artists enterprise communication mechanism which uses the data structure is also correct, and these proofs are publicly available and are run as part of the continuous

01:46:07.000 --> 01:46:19.000
integration to ensure the continued maintenance. next another example, is a foundational library called Big Number, which is used for hyp, precision, inter integer, arithmetic.

01:46:19.000 --> 01:46:26.000
That's about a 1,000 bits and most asymmetric, public private key cryptosystems like rse.

01:46:26.000 --> 01:46:30.000
Use these big numb libraries, and it's also used in something called S.

01:46:30.000 --> 01:46:44.000
2 N. S. 2 n tls is an aws implementation of tls as a cell protocols that's designed to be simple, small, fast, and with security as a priority, and there is a proof that it is free of side

01:46:44.000 --> 01:46:49.000
Channel analysis attack. And again, you can reference it online.

01:46:49.000 --> 01:46:55.000
So we move next. So we move from foundational code to the next level, and we move up the stack.

01:46:55.000 --> 01:47:00.000
And here it is about how we leveraging phone methods to ensure that the protocols are safe.

01:47:00.000 --> 01:47:16.000
Next. So one place we're looking at it is where are the critical systems. we have authorization cryptograph, and cryptography are the 2 main protocols that we are working to prove collect so kms is an aws.

01:47:16.000 --> 01:47:23.000
Managed service that allows a users to manage their cryptographic keys and control its use.

01:47:23.000 --> 01:47:37.000
Next. So we've been applying verification techniques to ensure that the protocols that describe how customer data is handled in transit and in rest holds true.

01:47:37.000 --> 01:47:49.000
Next, and we have machine checked proof that the cryptographic keys protecting customer keys are maintained securely across aws, and you have a paper on that.

01:47:49.000 --> 01:47:55.000
And the connection to Code and protocol is also checked continuously.

01:47:55.000 --> 01:48:02.000
Next, the protocol description proofs are open source, and you can independently verify them.

01:48:02.000 --> 01:48:05.000
So as you can see, there is a theme here where it's like, hey?

01:48:05.000 --> 01:48:12.000
We we the theme is we make open source what's available There's a tie to the code there is Ci CD.

01:48:12.000 --> 01:48:17.000
To instrument that they don't they are always insane.

01:48:17.000 --> 01:48:20.000
Okay, so we'll keep going up the stack next as we move.

01:48:20.000 --> 01:48:27.000
We, we wanna make sure that the applications where customer and user workloads and data run are also secure.

01:48:27.000 --> 01:48:41.000
So we'll continue with our encryption theme and we wanna close the loop and go on step further. So we want to ensure that all internal services that handle customer data and use these crypto api's are doing it

01:48:41.000 --> 01:48:55.000
securely. So here we use program verification techniques to ensure that the Service code in the Service code that all customer data is encrypted before it's stored log or pass to another service.

01:48:55.000 --> 01:49:00.000
Next. so we also are using it in different applications.

01:49:00.000 --> 01:49:06.000
So this is Amazon dot com That sold over 386 billion dollars worth of products to customers.

01:49:06.000 --> 01:49:19.000
And one of the things that requires to maintain this trust is the ability to safely and securely store critical payment information for all our customers, and we want our customers to trust us.

01:49:19.000 --> 01:49:31.000
So when they enter the data into these fields that it's secured correctly, and amazon's building a secure payment wall on aws.

01:49:31.000 --> 01:49:41.000
And it's using a lot of these technologies on proof, and the larger product than like proof of security to verify it.

01:49:41.000 --> 01:49:50.000
Next So just to good this was you you can just keep clicking to the end of the slide, because this is

01:49:50.000 --> 01:49:55.000
It's gonna be hard. I had some animation here. So at the root you have an Api call.

01:49:55.000 --> 01:50:06.000
We have the application that makes a request. The request must be allowed by some organization policies or permissions, and then we have the Im permissions that get attached to the resource.

01:50:06.000 --> 01:50:14.000
And finally, we have the network level, and the request has to get from the top, from the principle to aws over the network.

01:50:14.000 --> 01:50:23.000
And if you keep clicking through in order to secure our payment, we essentially have, like different analysis layers.

01:50:23.000 --> 01:50:27.000
We have network analysis, we have policy analysis, and we have coded analysis.

01:50:27.000 --> 01:50:34.000
And so e here's a way of like all the things I talked about, and how they get applied.

01:50:34.000 --> 01:50:41.000
So this is all internal right like we're doing all of this work internally to prove correctness of systems making it part of the development cycle.

01:50:41.000 --> 01:50:47.000
It's in continuous ci CD we're also using it to verify the stack of our entire applications.

01:50:47.000 --> 01:50:57.000
So i'm gonna talk next i'm gonna talk briefly about how it's gonna how it's actually being used in a lot of customer facing services.

01:50:57.000 --> 01:51:06.000
Next. So there's a the way we talk about this to end Users and customers is now with these services and features.

01:51:06.000 --> 01:51:21.000
They can make universal statements about their security. and we're talking about like quantifies like a cro none of my easy 2 instance are, and unintentionally public and all ssh traffic to my instances go through a

01:51:21.000 --> 01:51:30.000
firewall. Now, you and we look at this criterion we're like, Okay, how does it manifest the next?

01:51:30.000 --> 01:51:35.000
So this one is something called F. 3 block public access, and if you go to the S.

01:51:35.000 --> 01:51:38.000
3 console, and you look at a permission of a bucket.

01:51:38.000 --> 01:51:42.000
You'll see something called s 3 block public access and when you turn it on.

01:51:42.000 --> 01:51:47.000
It blocks all public access to the bucket. So what does it do under the hood?

01:51:47.000 --> 01:51:56.000
Can you click one? So it essentially translates the policy into an smt formula that checks.

01:51:56.000 --> 01:52:00.000
Does there exist some allow statement that violates my trust policy?

01:52:00.000 --> 01:52:05.000
So this is for the end user all they're doing is checking a box, a one check box.

01:52:05.000 --> 01:52:16.000
It's abstracting away all the complexity of having to specify an invariant or a specification, and ensuring that it's cutting it's all done under the whole 300.

01:52:16.000 --> 01:52:34.000
So and when it's when it's done when now, if a if a user tries to attach a policy that is not, that is public, there is a in line a simplest call made to the smt solver and the result of

01:52:34.000 --> 01:52:37.000
that smt solver gets bubbled up to the end user.

01:52:37.000 --> 01:52:44.000
So this is a big deal, because this synchronous, called an smt solver is in an Api of a control plane.

01:52:44.000 --> 01:52:50.000
Api of a low latency service, such as s 3 next.

01:52:50.000 --> 01:52:55.000
So we talked about like, Hey, you're the specification is embedded.

01:52:55.000 --> 01:53:11.000
But what about other services? So we provided this service call I don't have the I don't have the time to get into each of these, but we have a story for how each of these service does a lot of analysis under the

01:53:11.000 --> 01:53:15.000
hood and provides to the end user and abstraction.

01:53:15.000 --> 01:53:33.000
The access analyzer is one such a service that analyzes whether a user resources have public or cross-count findings, and we use stratified, predicate abstraction to ensure what are the set of sound findings that

01:53:33.000 --> 01:53:44.000
we return to a user next. We have other services for networking, such as Inspector.

01:53:44.000 --> 01:53:50.000
Next you know again we have a findings model it's like hey?

01:53:50.000 --> 01:53:53.000
You have a so you can see there is consistency.

01:53:53.000 --> 01:54:09.000
We are not launching multiple services with an inconsistent Format, because that adds more cognitive load to the user. Here, again, it's actually chalk checking properties that says, Hey does there exist a port where this property

01:54:09.000 --> 01:54:19.000
holds or it doesn't but it's presented to the user in a format that's consumable to them, and it matches their mental model.

01:54:19.000 --> 01:54:21.000
Actually I talked about this mental model, but it's like hey?

01:54:21.000 --> 01:54:32.000
You don't want to do it in a they represent you you don't want to do it in Ltl, which nobody will be able to use next

01:54:32.000 --> 01:54:44.000
So there's also i I talked about how we are doing it in a consistent format, and one of the keys is just a security hub that aggregates findings across different services next.

01:54:44.000 --> 01:54:54.000
And this is where, like universal statements that you're making about different parts of the Cloud assets come together next.

01:54:54.000 --> 01:55:00.000
So you see here, like the things that are true and access analyzer and things that are true.

01:55:00.000 --> 01:55:07.000
And inspector actually come together into like, Hey, This is what is not holding true of your system.

01:55:07.000 --> 01:55:12.000
And again. This is all in a way in a format that's accessible to them.

01:55:12.000 --> 01:55:17.000
Next. So the the the problem of like, how do we do?

01:55:17.000 --> 01:55:22.000
Specification, like keeps coming up, and part of it is again, How do we like?

01:55:22.000 --> 01:55:29.000
We are providing users, templates, templates, that they can fill in without having to understand logic.

01:55:29.000 --> 01:55:36.000
So this is again a part of if you look at the words it's like, identify access to Internet gateway example.

01:55:36.000 --> 01:55:48.000
And here all of these are in the way, getting you end users to write specification without them having to like know that they're writing specifications next.

01:55:48.000 --> 01:55:54.000
So it just. these are just different types of specification that they're writing without having to know.

01:55:54.000 --> 01:56:16.000
And next so 8 all of these you'll have to click through a few, because it's yeah get to the next slide, and all these services are allowing end users customers to be using formal methods under the

01:56:16.000 --> 01:56:29.000
herd without them having to be formal methods, experts, logicians, even computer scientists, because they are interacting with the service and the tool that they need.

01:56:29.000 --> 01:56:37.000
And want to use, rather than having to think about specifications and properties and proof systems, and all of those things.

01:56:37.000 --> 01:56:54.000
Next. So all of this is driving us using a So one other thing that I I didn't talk about is all of the customer facing tools that we talked about is using smt under the hood and what's that

01:56:54.000 --> 01:56:58.000
driving. It is like a 1 billion smt queries a day that next.

01:56:58.000 --> 01:57:03.000
And i'm gonna talk about a very specific challenge next about that we had here.

01:57:03.000 --> 01:57:10.000
So the engine here, I'm talking about zulcova It uses a portfolio solver to discharge its query.

01:57:10.000 --> 01:57:17.000
So Del Cova involves multiple solvers in the back end and uses the results from the result that returns first, and it's a winner.

01:57:17.000 --> 01:57:24.000
Take all strategy 2. So the portfolio approach allows us to really leverage the diversity among solvers.

01:57:24.000 --> 01:57:32.000
So we were like, Okay, we have a new solver. come out Cbc: 5, and we want to replace our Cbc for implementation with 65 next.

01:57:32.000 --> 01:57:39.000
So we we run it on a Next we run it on a large set of benchmarks to check its timeliness requirements.

01:57:39.000 --> 01:57:49.000
So this is just a representation representative set of queries across like 15,000, and we just select a distribution to show, like the queries that are sold between one and 30 s.

01:57:49.000 --> 01:57:56.000
And we see here that some of the queries that are not solved by Cbc.

01:57:56.000 --> 01:58:00.000
4 within the time bound of 30 s, are now being sold by Cbc.

01:58:00.000 --> 01:58:04.000
5 by the points in the graph along the Vi axis.

01:58:04.000 --> 01:58:10.000
On the extreme right, however. Cbc. 5 times out on some queries that are being sold by Cbc.

01:58:10.000 --> 01:58:13.000
4, as we see on top of the graph. So we next.

01:58:13.000 --> 01:58:17.000
So we worked with the Cbc developers and got this fixed.

01:58:17.000 --> 01:58:24.000
And but there was another issue here. Cbc. 4 was Twox faster than Cbc.

01:58:24.000 --> 01:58:28.000
5, for many of the easier problems that took 1 s to solve.

01:58:28.000 --> 01:58:39.000
Originally, and the results are not surprising. Given that the space is computationally hard, and there is an inherent randomness in search heuristics with an smt solver.

01:58:39.000 --> 01:58:51.000
But this was posing a challenge for us, because we are using the results of these solvers in security controls and services, and we can't have a regression and a solver impact customer. behavior.

01:58:51.000 --> 01:58:56.000
We saw all of these services. The point was like of showing those services is like.

01:58:56.000 --> 01:59:02.000
I cannot have my bucket go from, not public to public because my smt solver time dog.

01:59:02.000 --> 01:59:06.000
But then that end user hasn't done anything on their end.

01:59:06.000 --> 01:59:12.000
That would be a terrible experience for them next. So we we ran some experiments.

01:59:12.000 --> 01:59:19.000
So here's Cbc. 5 with the winner take all and portfolio solver without Cv. 5, and but Cvc.

01:59:19.000 --> 01:59:26.000
4 is part of the portfolio, and we see it doing well next, and

01:59:26.000 --> 01:59:28.000
We had a new version of Cvc. 5 with the winner.

01:59:28.000 --> 01:59:32.000
Take all, and portfolio solver and that's even doing better.

01:59:32.000 --> 01:59:37.000
So given that it led to our decision of next adding, Cbc.

01:59:37.000 --> 01:59:50.000
5 to the portfolio solvers, containing Cv. 4 Z. 3, and the sequence we have a custom sequence change solver, and the plan was never to add a new version, but because we expected to just the latest version of

01:59:50.000 --> 01:59:54.000
Cmc. 5 to be comparable in timeliness and correctness to Cmc.

01:59:54.000 --> 01:59:58.000
For, and and we did work closely with a lot of them.

01:59:58.000 --> 02:00:02.000
But yet we ended up adding to the server, So like, Okay, are we done?

02:00:02.000 --> 02:00:06.000
Not quite because we rinse and repeat, we are like the cycle repeats with Cbc.

02:00:06.000 --> 02:00:09.000
1.4. And now the question is, do we upgrade?

02:00:09.000 --> 02:00:15.000
Do we add it to another version to we and some of our early experiments is like, Hey, there, isn't a clear answer.

02:00:15.000 --> 02:00:27.000
Yet next. So we're like okay, we are the clown and what works when the cloud setting is a massive port for you, or sometimes even considering all versions of soul was there's 2 problems.

02:00:27.000 --> 02:00:32.000
Right. If we discover a bug in the older version of the solver, we'd need to patch that old version.

02:00:32.000 --> 02:00:45.000
And now this creates what's called an operational burden of maintaining many different versions of the solvents and 2 When the number of solar increases, we need to ensure that the each of the solvers is providing

02:00:45.000 --> 02:00:51.000
a correct result, now checking the correctness of queries inside the straightforward.

02:00:51.000 --> 02:00:58.000
But for smt solvers we need to provide proof for the Msat queries and the proof checking, and the proof.

02:00:58.000 --> 02:01:15.000
Generation needs to be timely as well next and next so i'm gonna in like i've talked about a broad set of things in a broad set of, and i've I have opportunities, misspelled but

02:01:15.000 --> 02:01:23.000
what are some of the things like? There are very interesting areas of research and opportunities for the broader area.

02:01:23.000 --> 02:01:28.000
Monotonous city and stability in runtimes of smt solvers.

02:01:28.000 --> 02:01:36.000
But essentially all analysis tools, because a little chain and we've known like, we accept it like, hey?

02:01:36.000 --> 02:01:41.000
We are in this computationally hard, pspace domain np-hard domain.

02:01:41.000 --> 02:01:46.000
And of course you're not gonna have consistency. But if we want to make it more mainstream.

02:01:46.000 --> 02:01:52.000
If we want to make it part of the development process, if we want to make it part of the Ci CD.

02:01:52.000 --> 02:01:59.000
The pipeline predictability is important. predictability in versions, predictability in upgrades approved generation.

02:01:59.000 --> 02:02:05.000
How do we know that the answer is correct? When now we are driving security controls?

02:02:05.000 --> 02:02:12.000
Based on the results of our tools. How do we just like a lot of the development of our tools has been on a very sequential world?

02:02:12.000 --> 02:02:16.000
How do we transition it to a distributed world like?

02:02:16.000 --> 02:02:21.000
Should. How do we make our tools themselves? leverage more of the micro services?

02:02:21.000 --> 02:02:30.000
Architecture such as the one that cloud computing offer better support for quantifiers in general.

02:02:30.000 --> 02:02:43.000
Thinking about developer tools and better usability. again, if we want to, have more developers using our tool as part of their workflow.

02:02:43.000 --> 02:02:47.000
How can we integrate better in the way that developers develop today?

02:02:47.000 --> 02:02:58.000
How it's Not an additional step they have to do I think that's gonna go a long way in driving a large scale adoption of such tools and services.

02:02:58.000 --> 02:03:03.000
One of my personal things is, how do we drive domain, specific verification?

02:03:03.000 --> 02:03:08.000
And how do we incentivize folks in academia to work on it?

02:03:08.000 --> 02:03:13.000
Because oftentimes we say, Hey, here's a paper this is great, but it only works for this domain.

02:03:13.000 --> 02:03:24.000
So, if it's not a general absence to work on just general or resolution.

02:03:24.000 --> 02:03:39.000
But for techniques to work, we have to leverage the domain, and if the domain is big enough, i'd love for us to find ways to infernalize a research in this area concurrency in mainstream tools like even

02:03:39.000 --> 02:03:46.000
like Daphne and other tools would be a great thing, and I learned on something called idiomatic compilation, like A.

02:03:46.000 --> 02:03:50.000
For for tools such as staff need to be used more broader and mainstream.

02:03:50.000 --> 02:03:53.000
Like either, we say, hey, run Daphne in production.

02:03:53.000 --> 02:04:02.000
But that would be a really hard sell. So because you know it doesn't have the required developers support, or you know, expertise.

02:04:02.000 --> 02:04:08.000
So if you generate if you're so saying hey? let's run the code that's generated from Daphne.

02:04:08.000 --> 02:04:11.000
It has to be something that developers can read, understand.

02:04:11.000 --> 02:04:17.000
So then they would be comfortable, saying, Hey, Yes, I know if i'm gonna operate this code.

02:04:17.000 --> 02:04:23.000
I know what this means. thank you again, i'm happy to take any questions.

02:04:23.000 --> 02:04:30.000
And on answer them and thank you. thank you, Edgar and Karen for helping.

02:04:30.000 --> 02:04:41.000
Yeah, thanks, That did a couple of questions. So Nate faster asks: So verification needs a model of the system, and the distributed systems are incredibly complex.

02:04:41.000 --> 02:04:45.000
So what models are you using, and how you check that?

02:04:45.000 --> 02:04:56.000
They like reality. Yeah, and that's a great you know point where this is web connecting to the code is very important.

02:04:56.000 --> 02:05:12.000
Where and how it's through some differential testing approaches where it's like, hey generate tests on the model generate tests on the code and try to ensure that there is a conformance taking models turning

02:05:12.000 --> 02:05:22.000
them into runtime monitors so there's also one area where we are saying, the model is the system.

02:05:22.000 --> 02:05:26.000
So that the actual system code is generated from the model itself.

02:05:26.000 --> 02:05:38.000
So we are doing it. in a couple of areas the encryption. Sdk: is using a daphne model and generating code like Java code, and go code a dot net code from from the Daphne model itself. So here.

02:05:38.000 --> 02:05:44.000
It's. The model is essentially not like an abstract model, but a representation of the behaviors.

02:05:44.000 --> 02:05:59.000
But there, isn't, a one there's no I I mean i'm preaching to require. but of course there's no silver bullet right like and one of the things is we should not view verification as an all or none law

02:05:59.000 --> 02:06:08.000
like, How can we, inject more development techniques based on testing validation?

02:06:08.000 --> 02:06:13.000
To start to make the bridges between the model and the code and the like.

02:06:13.000 --> 02:06:22.000
The tests are great. the test that end users right are a great example of in a way specification so like, how do we use that?

02:06:22.000 --> 02:06:25.000
So I think, leveraging more of that, and will help.

02:06:25.000 --> 02:06:30.000
But it requires building a lot of tooling and building a lot of infrastructure to make that happen.

02:06:30.000 --> 02:06:38.000
Okay. There are actually a couple more questions from Matthew Bolton.

02:06:38.000 --> 02:06:47.000
Is there a cognitive theory gender design principle behind a war usable user specification are defined.

02:06:47.000 --> 02:06:59.000
If it's based onmented models how do you know that the human mental model is Yeah, that's a interesting aspect with

02:06:59.000 --> 02:07:04.000
The constructs we've ended up using are based on the domain?

02:07:04.000 --> 02:07:13.000
So how do security engineers talk about constructs like It's through talking to a lot of and this is also some.

02:07:13.000 --> 02:07:20.000
It's called something called persona based and the personas are different, like who's doing what task you have security engineers.

02:07:20.000 --> 02:07:28.000
You have developers. you have it Adm. administrators, and based on how we come up with the mental model.

02:07:28.000 --> 02:07:31.000
Is. each of them have a defined like, Hey, This is their job.

02:07:31.000 --> 02:07:34.000
This is their workflow. This is what they go through.

02:07:34.000 --> 02:07:42.000
If and we translate them into these higher level constructs of for a for a developer or security engineer.

02:07:42.000 --> 02:07:55.000
The notion of I have a finding about like the city that's related to the security of my system that matches their mental model of what they're doing, because, like findings are things that come in pen tests and like abstract reviews

02:07:55.000 --> 02:08:00.000
it gets generated. so like if you said here's a violation of your property.

02:08:00.000 --> 02:08:05.000
Also in like here's the potential counter example that would not make any sense.

02:08:05.000 --> 02:08:13.000
But here's a finding that demonstrate this account can access your resource under these conditions.

02:08:13.000 --> 02:08:27.000
So there, isn't a gin generic cognitive theory, but it's really related to who the product is targeted for like what's their role in their company?

02:08:27.000 --> 02:08:38.000
And how how they how they go about doing their job, and then matching the constructs and the tools for that Actually, more questions.

02:08:38.000 --> 02:08:46.000
But we are kind of over over time, and we've been hoping actually for some discussion for everyone.

02:08:46.000 --> 02:08:51.000
But so let me just take one question, which is, for all of you.

02:08:51.000 --> 02:09:02.000
This is from getting Walker. So one way to incentivize academics, maybe to supply open challenge problems with charity data sets.

02:09:02.000 --> 02:09:10.000
And the Academics need real world data which can be difficult to obtain unless we have personal connection to industrial partners.

02:09:10.000 --> 02:09:20.000
So if any of you want to, you know, address this. that would be great.

02:09:20.000 --> 02:09:33.000
Okay, I think Smt: Comp is a great model, and has, you know, benchmarking and competitions always have a dark side of occasionally pushing research in the wrong direction.

02:09:33.000 --> 02:09:37.000
But on balance it's been a great sanity check and a great way to drive research.

02:09:37.000 --> 02:09:52.000
And as you know. I think sons people in industry ought to be motivated to work with academic partners to get benchmarks into that, because then you've got all kinds of people hammering on whatever problem

02:09:52.000 --> 02:09:58.000
you you came up with. and so that was one of the things we did with Cvc.

02:09:58.000 --> 02:10:07.000
5 was we, since since our system was open source. Anyway, we we could take the problems we were running into that were problematic.

02:10:07.000 --> 02:10:18.000
Give them a collection of benchmarks for vectors and other things, and they could try to use that for Cvc. 5. and then we got permission for them to share that in the competition.

02:10:18.000 --> 02:10:29.000
So that's something that I would highly recommend for anybody who's a user of Smt Solvers that is having some struggles.

02:10:29.000 --> 02:10:36.000
So to what David said. we did the same right like we have like our examples of what a hard benchmarks with the Cbc. team.

02:10:36.000 --> 02:10:46.000
One of the things, though. is there is a there's a dual side to the coin of like leading benchmarkets. A.

02:10:46.000 --> 02:10:50.000
You know there is a process that goes through like, Hey, what are the benchmarks being supported?

02:10:50.000 --> 02:10:59.000
2 we like parts of it is so here's what I would love to like.

02:10:59.000 --> 02:11:05.000
Think about synthesis approaches, or generation of benchmarks, or just, you know, getting more.

02:11:05.000 --> 02:11:22.000
Diversity like sharing is one approach. but thinking about how to benchmark techniques, how to think about especially with respect to monotonicity I love for the Smt com to have a new category

02:11:22.000 --> 02:11:36.000
where it takes into account how you did last year. on these sets of benchmarks, right? like, Because right now the incentive is to solve more problems and solve how the problems which can allow the tools to regress on yeah

02:11:36.000 --> 02:11:39.000
the previously saw, like the performance of previously on again.

02:11:39.000 --> 02:11:44.000
And I understand these are hard problems like I. I understand why, theoretically it happens.

02:11:44.000 --> 02:11:52.000
But that to me, I think, would be would be one way, but also looking at synthesis of bridge box like, how do?

02:11:52.000 --> 02:12:01.000
Just even using the shuffler right like we say, Hey, we We can create such a huge variance in the

02:12:01.000 --> 02:12:16.000
The runtime. So I I think, indeed, in general, and this maybe this is something like the tool development process, and I think the Cbc team is a great example of it.

02:12:16.000 --> 02:12:26.000
But You know where the the challenges for academics are in publication, to apply tools at an industry level.

02:12:26.000 --> 02:12:33.000
You have to invest in tool development, and of course you know that is that there's the cost associated with it.

02:12:33.000 --> 02:12:40.000
And industry should be funding it, but also like

02:12:40.000 --> 02:12:54.000
How to ensure that there is a path for success both in terms of publication as well as external government funding for these, for academics like, I think it's it needs to be a combination of all 3 for for

02:12:54.000 --> 02:13:10.000
us to push. and I when I say tool development I don't necessarily just mean engineering, right like, but making robust tools like a that take over years to get there.

02:13:10.000 --> 02:13:16.000
Okay. So let me ask one final question again. You know other few.

02:13:16.000 --> 02:13:25.000
So I think. it seemed like, you know, the the solution to folks not ingenious, not clearly understanding problem.

02:13:25.000 --> 02:13:36.000
Space specification. The solution that you, many of you, seem to be able to be advocating is that we come up with this pattern or something, but the other one could be actually incentivized.

02:13:36.000 --> 02:13:42.000
You know, undergraduates to learn a bit more about department specifications and listening.

02:13:42.000 --> 02:13:55.000
And when chat that we face in academia is that in the industry recruiting process seem to incentivize, studying our marketing, thinking but very little about in a formal logic and specifications.

02:13:55.000 --> 02:14:07.000
And so on. So I wonder if it is any any way, you folks can help questions about this into the interview process.

02:14:07.000 --> 02:14:15.000
Basically. Yeah, yeah, and it's a bit of a chicken and a leg problem like we can't hire engineers would, you know, could could be able to write specific stable for internal things.

02:14:15.000 --> 02:14:20.000
And there's a lot. We go through and so we should think about how we can see it.

02:14:20.000 --> 02:14:43.000
And pilots and programs around this we're pushing it under the in like undergraduate education programs with the path to future jobs

02:14:43.000 --> 02:14:52.000
You you say that the there's emphasis of algorithmic thinking that might reflect on people who are conducting interviews.

02:14:52.000 --> 02:14:58.000
If you get an algorithmic interview and and it.

02:14:58.000 --> 02:15:14.000
But the reality is, of course, that in in a job situation. you'll you need a combination of algorithmic and and formal thinking, And so I think it's a question of it's stealing a the

02:15:14.000 --> 02:15:19.000
culture.

02:15:19.000 --> 02:15:24.000
Yeah from from audit, I think, having a background in formal specification.

02:15:24.000 --> 02:15:36.000
And yeah, you know, that sort of background is definitely a plus. And much of our, you know, developers who work on this sort of pipeline have Phds in either programming languages or follow verification.

02:15:36.000 --> 02:15:48.000
So would say, for that team but definitely it's beneficial, and we have incentives for the right kind of Ion

02:15:48.000 --> 02:15:55.000
Okay, Thank you. I think we are getting over the time. But thank you. Thank you.

02:15:55.000 --> 02:16:03.000
And This was wonderful. and we, you know we had, as you can see we.

02:16:03.000 --> 02:16:07.000
You know we had participants from all over. This is the end of this session.

02:16:07.000 --> 02:16:23.000
So you know the for those of you who are not part of the and they said, program, You know, we have a session tomorrow at 2 o'clock, and we're welcome to join that using the same link we're just

02:16:23.000 --> 02:16:26.000
focusing on future directions and those who are part of the bi meeting.

02:16:26.000 --> 02:16:46.000
I I guess the next session starts at 2 o'clock, and you can to join using the this. the other thing which was for the closed session. and then they will have ring I think it sounded so thank you thanks