Hello everyone, I'm Maxine, I'm from France, and I'm working at an area in Orande as the
Pages student.
So I started recently, and last year when I discovered the BFF, I had the opportunity
to make a performance evaluation of the BFF earlier, and I learned something on it, and
today I will show you some submissions I made.
So I started by making some differences between some kind of versions, and then I'll compare
the BFF earlier with prevail because it gives a comparison point.
So this is simple representation of the BFF earlier, so it is a static analyzer.
It verify the behavior of the received program inside the kernel, and it checks that the
set of specification, like not jumping outside the instructions or leaking canal data.
I do the two-step verification, it starts by working on the instruction to check if there are
on which are the instructions or back edges, if you don't have capabilities, and this case,
it's subject to your program. And the second step is to verify the behavior of the program,
so it's up with the set-pron, and then the prime, and if the prime is accepted, it is then
compiled, and attached to a hook point, waiting for an event to trigger the prime.
Although there are new features, I've been added, and the behavior is getting more complex.
Some bugs could be introduced, and it is complex components. It is out to assure the safety
of the entire kernel, and of the BFF earlier, because it is complex, and it is not some
added defined, and it is not well documented. And the BFF pair can also reject point, which would
be active, so it does fast-spelitude. However, since few years, BFF has been an active research
wheel, some works have been done on phantom bugs, so dynamically using fuser, or statically,
with, for example, active, which uses the same fuser. It's our observation, using software and
hardware-based approach, which is in telemplk or RMT. There are two other methods to verify
problems, which have been proposed like prevail. Proball is another of the failure of BFF problems,
introduced in 2019, it is used on some projects, and it is used on Windows, so I'll come back
a bit later to the prevail, in the second part of the talk. So, BFF exists on the list,
it can have since 2014, and since the years, or many modifications that have been made on the
VFAR, and some of these modifications could have an impact on the performance of the VFAR.
So, we are going to check all the some versions of the VFAR BFF's, in terms of the
execution time, and the more we could print and power correction. For our experiment, we use
version of Ubuntu, so we start this channel for .NETing to 6.10. We use a set of pre-compile
problems from the array repository, and since some of these problems contain custom sections
and legacy maps, we use prevail as a loader for the VFAR. However, previous, they do the bad
problem type for some of these problems, which is the VFAR to reject the problem for a bad context
or bad elders. So, I just remove our distance, I use only one of the great info
different problems for my test. This figure shows us the very same time of that type of
programs, encouraging the number of instructions. And we can see that for print with less than
1, 0, and 6, 100 instructions, the verification tape for all the VFAR seems the same. However,
with larger programs, we can observe that for the candidate 4.8 mentioned, the verification
time is higher. It can be explained in part because more functions were generated on this channel.
The second figure shows us this time the memory should print, according to the number of
instructions of the attempted programs. And we have actually the same observation that the memory
footprint of the 4.8 is higher than the other. I observe that the VFAR in 4.8 is generated
for this range of instructions, like seven or eight more branches, which imply that some
instruction would be the effect multiple times, and it requires more memory to sort of branches.
I am going to check how many prints were accepted by the VFAR. And we can see that
none of the VFAR accept all the poems. However, if we check at the second part of the table,
we can see that there are six reasons for the first one is complexity limit, which is
reached for the 4.9 soon. There are also bad candidate configurations or a lockdown mode, but if
we manage to solve all these issues, we can see that the VFAR accepts all the programs of
accept one because of the complexity limit. So the idea is that the VFAR is not always to
play for the rejection. It can be a bit more than just the VFAR. It can be a kind of configurations
of the way you load your programs. Now, as a comparison, the VFAR was prevailed.
As I said, the VFAR of the VFAR programs is being published in 2019, and it was in user space
compared to the VFAR, which means it can be expressed in terms, because it uses an absolute
domain which requires more memory and time to execute. So the abstract domains are used to
represent the values on the abstract world, so at the advantage of the time. So in the store,
values are in our constraints, so it keeps information between them. In court reasons,
the VFAR uses the interval domain, so it's the interval of values with the minimum in the
maximum bond, and the TNU, which stands for sophisticated numbers, which add some bit precision with
the mask. So the mask indicate if a particular bit in the value is known or unknown, if it is a known,
it can be zero or one. There are some different things the way past these are managed.
On the VFAR since many bunches are very failed, the state printing has been added to
reduce the number of bunches, so the bunches is very failed, so the very failure starts on the
checkpoints, and when it's very fun as a bunch, if it finds that the current bunch of states,
which is the same as one checkpoint, it can detect the bunch, otherwise it will be the same,
which it helps to reduce by the number of bunches. In court, I don't prefer to use a general
parameter, which means that when two bunches are meeting at the same instruction, it just
melts the values. The same thing also, differentties in the way loops are handled. The VFAR will
loop on the, when it will deteriorate over the loop, until the condition is very failed, and it will
generate possible a lot of bunches, while prevail use the fixed-point computation, it means that
when you find a fixed point between two different loops, it can just leave the loop and continue
to verify the rest. The rest was some things to say about the sum this. We have seen that
symbols have different on the VFAR file, and some makes state, and as I said, this is not for
many differentties, it's hard to understand, so it's hard to prove the failure entirely, so we
don't know if it's really insane or on some. For prevail, by design, it should be sound, however,
as the implementation is different than the design, it could contain bugs, so we don't really
know for prevail. Now we're going to see how the VFAR behaves against prevail in terms of
verification time in my construction and accepted programs, because it deserves a comparison point.
So, I did the same point as before. I use the KFAR-13 and 6.10. The first version of prevail,
which is the KLDI preparation, will run on the 4.910, and the lattice will run with the KL-6.10.
This figure shows us the verification time of the accepted programs, according to the number
of instructions of this program. And we can see that for larger programs prevail, we have
a lot more times to verify the print, like eight or nine more seconds like the VFAR.
It's in part due, because of the zone domain, you go to each other, you have more times to
execute, compare to the interval or tenium. This figure, so this is the memory, if we'd print
of the programs. And we have the same remark as before that prevail, because you're more memory
to verify the print. However, we can see that between the selection of KL and the lattice one,
you have a huge difference in terms of a very construction, like one gigabyte. It's because
when prevail was presented, it uses some ethanol libraries, and now all this stuff isn't
produced in the source code, which I used it's memory usage. It's good.
So, previously, we saw the number of accepted programs for here, let's say, let's say,
about prevail, prevail, at one goal, also, which is reduced the number of false
politicians. You can see that for the subversion of prevail, there's one rejected program
if it's a letter version, there are four rejected programs. It seems that there are a
regression. If you look at the second table, it shows the number of rejected programs by
inventory in the left column, which are accepted on the source code by a very failure. We can see
that the source from the rejected by prevail are accepted in the fourth version of prevail.
And all the rejected programs by both the version of prevail are accepted by the units.
So, prevail at a regression, in terms of accepted programs, and it's a refight left
for them, and the decayed very failure, for this set of samples. Now, I'll show you some differentties
on the way the refighted by this mini-passes. I'll use the new SRMP template from the
pre-alienery predatory, because it's interesting. It contains two non-unroll loops, and some if
else in it, and I will configure the number of loop iterations, which he has the very failure
will indulge the number of loops. So, the two figures are the verification time, and the
memory footprints, I can't need to do the number of the loop iterations. And you can see that
while prevail at a fixed point earlier, the B.P. is like I have continued to increase
the verification time, until reaching the context limit at around 155 loop
iteration value. And we can see that the memory footprints seems the same, or is
nearly the same for the number of loop iterations, for the very failure. We can see also that the
sub-partient in the U.K.L. project programs is because the band-aid loop verification was
added in 5.3. And for prevail, I don't know if they are rejected, in the paper, they said that
they should be accepted, but as they didn't give us information, the compiler they use,
it can be because of this. So, I learned to for this time. To conclude, we saw that the purpose of the
very failure has improved over the versions of the, of the, of the candidate. We have sort of no
regression, which is a good thing. And the point prediction is not only limited to the B.P.
life I have already said, it could be larger than this. It was an interesting approach to the
band-aid loop verification with the fixed-print computation. And the association that prevails
have reduced its memory, which is a good thing. However, it seems that there is a regression
with the added version of prevails, but it would require physical investigation, because it
was not one of my main ideas for the talk. Thank you, everyone, for your time joining.
I hope it was interesting, and now we look for questions for the last minute.
The question is, which version I use on mid-camera of prevails? I do the fourth version of prevails
in the fourth-print painting, because it was, you can't use the experiment of the paper. And
I use the original prevails on the sixth-print painting, because it was as a time by doing the experiments.
So the difference is, like, in terms of program rejections or acceptance, it's like in terms of the
evolution of prevails. Yes, it's not due to the camera. Yes.
So it's not due to the problem. It's not due to the problem.
In terms of usability, it's not due to the problem.
You see some error, for example, it was the error on the stand where
the program rejected these more in the third-print painting. So the idea is, those prevails are
better old-put in terms of already. Personally, as I use sometimes a BPS on early news,
I understand more of the old-put of the very fire when there are rejections.
The privilege of you something linked to the linear conference, so it can be a bit complicated to
ignore them.
About the rejected problem?
I don't do the rejected actually.
I see that I saw a commit, it changes something on the
verification. At the moment, where the
pre-invariant, we are perhaps to the post, but I did it in your family, what is the purpose of this?
It's not the time the memory comes out.
It's the previous one, a couple more of it.
Yes. So what can you explain, so did the character that can
this is one gigabyte?
Yes.
The command which I couldn't get back in 400, 500 gigabyte.
For the time being, this character is pretty normal for the
question, like, 200 megabyte, 200 megabyte.
I also say that when there are more inspiration to verify,
it will pay a lot more memory. I tested the
double-surfing pay template, with not only loops, and at each
iteration, we can have more memory to verify the prompt.
I use some, I use some, an old version of the
one, and I add more and more instructions, but I did not add the
time to put it on my search.
Someone else?
What would you say is the conclusion of your work, so what would you say,
something about whether it should use the name, the kernel, or the
system about the actual evolved, what is the very
higher level of the memory consumption of frevel,
as soon we can't really use it, and I thought it turned
into a user space, but maybe we could use some of its
mechanisms to improve the data.
Try to be an agent.
Thank you.