Interpretation-Based Violation Witness Validation for C: NITWIT
CC Attribution 3.0 Germany:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Berger, Philipp
As software verification is gaining traction in academia and industry the number and complexity of verification tools is growing constantly. This initiated research and interest into exchangeable verification witnesses as well as tools for automated witness validation. Initial witness validators used model checkers that were amended to benefit from guidance information provided by the witness. This approach comes with substantial overhead. Second-generation execution-based validators traded speed for reduced strength in case of incomplete and non-exact witnesses. This was done by extracting test harnesses and compiling them with the original program. We present the NITWIT tool, a new interpretation-based violation witness validator for C programs that is trimmed to be fast and memory efficient. It verifies a record number of witnesses of SV-COMP'20 in the ReachSafety category. Our novel tool exchanges initial compilation overhead and optimized execution for rapid startup performance. NITWIT borrows C semantics from the compiler used for compilation. This offloads this hard-to-get-right task and enables using several compilers in parallel to inspect possible semantic differences.
 Hello and welcome everyone. My name is Philipp and I will tell you about NITWID, our interpretation-based violation witness validator for C code. First bit of background about witnesses and model checking. So what you might be familiar with is that with a typical model checker, you have an input. In our case, it's a C program and you have a property. We are, for example, interested in reachability properties. So if an error state is reachable or not, and you feed both of these the program and property to model checker, and in the end you will get a result and the model checker will tell you either that the property is fulfilled, it's not fulfilled, or it simply doesn't know because of an error or a timeout. In recent years, there is an additional output available from many model checkers which is called a witness. And what is this witness? Witness, you might be familiar with certificates in complexity theory. So the witness in the case of model checkers is basically trying to or should encode everything that the model checker learned while doing the verification, everything it generated for instance invariance or simply decisions it made to reach certain states in the program. So the idea is that with the witness in hand, retracing the steps that the model checker took should be easier. So the verification should be easier. The next time around, there are currently two types of witnesses available. One is for reachability properties that are violated. So these are violation witnesses. And the other one are of course then the correction witnesses for a model checker testing that a property is indeed or a state is unreachable. A simple example for a violation witness would be in the program depicted on the bottom, the violation witness could encode the path shown in red towards the error state. So there are decisions that were made and these are then encoded in the witness. Our focus is of course on violation witnesses as the title already implies. And for violation witnesses, we can say that they can restrict the state space of the program that is analyzed. They can provide resolution of non-determinism and they can guide the search towards the error location. The problem is the can at the beginning because what is shown on the bottom now is also valid violation witness, which is simply telling us that an error state is reachable at some point in the program, but nothing more. So regarding motivation, our situation at the beginning of developing nitwit was the following. We were testing open source model checkers on some C code that we sourced from the automotive industry. The C code in question was quite large, so 120 kilobytes per file. We had a lot of properties, so in the end we were interested in verifying properties on around 1,000 instances of these code files. And we had a problem because we got conflicting results. And of course now we thought, okay, what to do with conflicting results? And as you might already have imagined, the answer is of course witness validation because if you have these model checkers that produce witnesses, you can just use the witnesses to verify whether property actually holds or maybe it's just a spurious error in the model checker. There is a problem because back then we only really had two violation witness verifiers, namely CPA checker and ultimate automizer, which are model checkers that could use the witnesses to enhance their verification attempt. I said enhance, but we observed that the witnesses didn't really strengthen the tools, so both of the tools basically performed their standard model checking procedure using the witnesses as enhancement, but the time and complexity that it took them did not substantially decrease by using the witnesses. There were also some other problems that we encountered. So here are two examples, one is that we had CBMC, Abundant Model Checker, detect property violations, so CBMC said an error state is reachable, but CPA checker on the other hand established correctness on the same property and program. So we encountered the problem that at least back then the witnesses generated by CBMC were not in the right format that CPA checker or ultimate automizer would accept. Another issue that we encountered was that the tools simply didn't agree, so CPA checker and ultimate automizer had different answers. And if these tools are also the only ones available for validating witnesses, do I really trust their witness verification? And as I said earlier, if they basically just use their normal model checking procedure, can the result really differ based on the supplied witness? And in our case, it didn't. Another problem is that the entire procedure, as I stated earlier, is very time and memory intensive, so if you want to validate the 1000 properties that we were interested in, which will basically, back then, it would take you as long as it took you to validate the original properties with the model checkers. So we came up with NITWID, which stands for Interpretation-Based Violation Witness Validator, and this is a new execution-based validator. So it's not, for example, a CPA checker or ultimate automizer, a full-blown model checker, and it only explores a single path through the program because it just interprets and executes the program. Because of this, it's also quite fast and memory efficient, and because it supports a lot of the basic C99 standard elements, it's applicable to a lot of C programs, for example, the entire, or almost the entirety of the SVComp C program set. How does it work? How is it implemented? Basically we have, on the one hand side, the interpreter driving everything and working on the C code, and on the other hand, we have the witness automaton that we generate from the supplied witness. And we use these two in lockstep, so the interpreter goes through the program, and at every point in a program where we could derive control flow edges, or where, for example, we go into a function, we return from a function, we set a variable, we declare a variable, we will hand this information over to the witness automaton, the witness automaton will check if this is also represented in the witness, and if this is represented in the witness, for example, if there is information on how non-determinism is resolved, so how a decision is made, this information is then fed back into the interpreter, the interpreter will resolve the non-determinism in its internal program state and continue execution. At some point the interpreter will either reach the error marking and return false, which marks that this is indeed a correct violation witness, or it will terminate or run out of memory or time and return the result unknown. There are some things that are quite nifty in our approach with the interpreter, for example, if you need to check assumptions, so one example would be states-based guards in the witness that restrict where you go in the program or that resolve non-determinism are quite easy to do in the interpretation approach, because you can just clone the entire state of the interpreter and then have the interpreter interpret the states-based guard in your violation witness in the context of the current program, as if it were an if statement, for example, in the program. Extract whatever is, for example, resolved in terms of non-determinism, and then simply restore the origin state that we copied of the program. Something that I've told you about is based on PicoC. PicoC is a C interpreter originally designed to work in embedded systems that is available for free online, but for our use case it didn't support enough of the C standard. So we added quite a number of features and functions. Of course, a lot of these are not strictly required, for example, in its original use case. So, for example, the callbacks to extract information about program states and where we are in the program, what functions are called, or also the non-deterministic types and function support isn't necessarily part or doesn't need to be part of PicoC, but, of course, it's required for our use case. And to give you a bit of an overview about how NITWIT performs, we have collected the results from the recent SVComp 2021. Here you can see all the six validators that participated in SVComp 2021. Blue means that a witness was successfully validated as a correct violation witness. So these presented witnesses are only the violation witnesses. And as you can see, for example, here NITWIT only shows blue and unknown or a timeout. So we don't have the green color for true because NITWIT can never decide that a program holds because it only explores a single state through the program. So this is in stark contrast to, for example, CPA checker or ultimate automizer. To give you a bit more information on how NITWIT performs, you can see time consumption plotted over the witnesses. So what you can see is basically that because we're using the interpreter approach, we have a very, very low overhead for program start and setup, which you can see that, for example, the next runner up in terms of startup time is the C-Prover witness to test program, also called F-Shell, which is two orders of magnitude slower in initial startup and overhead than NITWIT is. Of course, C-Prover uses a similar approach to ours just that they use compilation in the beginning. So they first compile the program and then execute it instead of interpreting right from the start. And that's a trade-off because if you have a large program, the compiled program will be a lot faster than the interpreter will ever be. And you can clearly see that in how linearly it scales over larger programs, whereas NITWIT starts taking up more time quickly with larger programs. If we look at memory consumption, we can also see NITWIT has the advantage of the low overhead, but of course, with larger programs, its memory consumption grows as well. Here you can see an n-dimensional Venn diagram for coverage. So this tells you which witnesses were covered by what tool. We can see that, interestingly enough, there is something special for everyone. So every tool has a couple of witnesses that only this tool really covers. So every tool is a necessary and welcome addition to the pool. At least that's what I would conclude from this. Looking at the numbers, on the left you can see which verifier generated the witness and then the columns tell you what tool could validate how many of these generated witnesses. And one interesting takeaway I would say is that, of course, every tool is usually the best verifier for its own witnesses. So if you look at CPA checker, generated 1,293 witnesses, 1,327 witnesses, as seen in total on the right, and CPA checker could validate 1,216, which is, of course, again a hint that the witnesses are not always strong enough to really make the validation possible even for the original tool. And we can see a similar thing, for example, with Ultimate Automizer, which, as Marty and Bolt could also verify the most witnesses of itself. So to sum this up, we had a data set of 12,873 witnesses in total from REACH safety properties in the recent SVCOM. We could validate 8,100 of those successfully with NITWIT, which is the most under all participating tools. If we look at a bit of timing statistics, so for example, only on witnesses that were successfully validated, we can see with the median time of 16 milliseconds, NITWIT is blazingly fast. If you look at the average, of course, it's a bit slower because of programs that get larger and larger. Remember the overhead tradeoff with the compilation. If we look for comparison on all witnesses, so also those that we couldn't validate where we, for example, ran into timeouts, which is, I guess, our biggest loss factor there, you can see the median climbs slightly, but the average climbs a lot more. And the same also applies for memory. So in median, we only take about two megabytes, but of course, for the larger programs, you can see in the standard deviation, we will take a lot more. So in summary, our contribution is a new validator for violation witnesses called NITWIT. It's available on GitHub. It's open source and free. It's quite fast. It's independent of existing model checkers. So if you don't trust them, you can use NITWIT. It borrows semantics from your compiler. So you can use different compilers to get an insight, for example, in differences between compilers. It supports 32 and 64-bit programs. There's a lot more options available using compile time flags, and maybe in the future, we will also implement witness refinement within NITWIT. Thank you.
 Hello and welcome everyone.  My name is Philipp and I will tell you about NITWID, our interpretation-based violation  witness validator for C code.  First bit of background about witnesses and model checking.  So what you might be familiar with is that with a typical model checker, you have an  input.  In our case, it's a C program and you have a property.  We are, for example, interested in reachability properties.  So if an error state is reachable or not, and you feed both of these the program and  property to model checker, and in the end you will get a result and the model checker  will tell you either that the property is fulfilled, it's not fulfilled, or it simply  doesn't know because of an error or a timeout.  In recent years, there is an additional output available from many model checkers which is  called a witness.  And what is this witness?  Witness, you might be familiar with certificates in complexity theory.  So the witness in the case of model checkers is basically trying to or should encode everything  that the model checker learned while doing the verification, everything it generated  for instance invariance or simply decisions it made to reach certain states in the program.  So the idea is that with the witness in hand, retracing the steps that the model checker  took should be easier.  So the verification should be easier.  The next time around, there are currently two types of witnesses available.  One is for reachability properties that are violated.  So these are violation witnesses.  And the other one are of course then the correction witnesses for a model checker testing that  a property is indeed or a state is unreachable.  A simple example for a violation witness would be in the program depicted on the bottom,  the violation witness could encode the path shown in red towards the error state.  So there are decisions that were made and these are then encoded in the witness.  Our focus is of course on violation witnesses as the title already implies.  And for violation witnesses, we can say that they can restrict the state space of the program  that is analyzed.  They can provide resolution of non-determinism and they can guide the search towards the  error location.  The problem is the can at the beginning because what is shown on the bottom now is also valid  violation witness, which is simply telling us that an error state is reachable at some  point in the program, but nothing more.  So regarding motivation, our situation at the beginning of developing nitwit was the  following.  We were testing open source model checkers on some C code that we sourced from the automotive  industry.  The C code in question was quite large, so 120 kilobytes per file.  We had a lot of properties, so in the end we were interested in verifying properties  on around 1,000 instances of these code files.  And we had a problem because we got conflicting results.  And of course now we thought, okay, what to do with conflicting results?  And as you might already have imagined, the answer is of course witness validation because  if you have these model checkers that produce witnesses, you can just use the witnesses to  verify whether property actually holds or maybe it's just a spurious error in the model  checker.  There is a problem because back then we only really had two violation witness verifiers,  namely CPA checker and ultimate automizer, which are model checkers that could use the  witnesses to enhance their verification attempt.  I said enhance, but we observed that the witnesses didn't really strengthen the tools, so both  of the tools basically performed their standard model checking procedure using the witnesses  as enhancement, but the time and complexity that it took them did not substantially decrease  by using the witnesses.  There were also some other problems that we encountered.  So here are two examples, one is that we had CBMC, Abundant Model Checker, detect property  violations, so CBMC said an error state is reachable, but CPA checker on the other hand  established correctness on the same property and program.  So we encountered the problem that at least back then the witnesses generated by CBMC were  not in the right format that CPA checker or ultimate automizer would accept.  Another issue that we encountered was that the tools simply didn't agree, so CPA checker  and ultimate automizer had different answers.  And if these tools are also the only ones available for validating witnesses, do I really  trust their witness verification?  And as I said earlier, if they basically just use their normal model checking procedure,  can the result really differ based on the supplied witness?  And in our case, it didn't.  Another problem is that the entire procedure, as I stated earlier, is very time and memory  intensive, so if you want to validate the 1000 properties that we were interested in,  which will basically, back then, it would take you as long as it took you to validate  the original properties with the model checkers.  So we came up with NITWID, which stands for Interpretation-Based Violation Witness Validator,  and this is a new execution-based validator.  So it's not, for example, a CPA checker or ultimate automizer, a full-blown model checker,  and it only explores a single path through the program because it just interprets and  executes the program.  Because of this, it's also quite fast and memory efficient, and because it supports a  lot of the basic C99 standard elements, it's applicable to a lot of C programs, for example,  the entire, or almost the entirety of the SVComp C program set.  How does it work?  How is it implemented?  Basically we have, on the one hand side, the interpreter driving everything and working  on the C code, and on the other hand, we have the witness automaton that we generate from  the supplied witness.  And we use these two in lockstep, so the interpreter goes through the program, and at every point  in a program where we could derive control flow edges, or where, for example, we go into  a function, we return from a function, we set a variable, we declare a variable, we  will hand this information over to the witness automaton, the witness automaton will check  if this is also represented in the witness, and if this is represented in the witness,  for example, if there is information on how non-determinism is resolved, so how a decision  is made, this information is then fed back into the interpreter, the interpreter will  resolve the non-determinism in its internal program state and continue execution.  At some point the interpreter will either reach the error marking and return false, which  marks that this is indeed a correct violation witness, or it will terminate or run out of  memory or time and return the result unknown.  There are some things that are quite nifty in our approach with the interpreter, for  example, if you need to check assumptions, so one example would be states-based guards  in the witness that restrict where you go in the program or that resolve non-determinism  are quite easy to do in the interpretation approach, because you can just clone the entire  state of the interpreter and then have the interpreter interpret the states-based guard  in your violation witness in the context of the current program, as if it were an if statement,  for example, in the program.  Extract whatever is, for example, resolved in terms of non-determinism, and then simply  restore the origin state that we copied of the program.  Something that I've told you about is based on PicoC. PicoC is a C interpreter originally  designed to work in embedded systems that is available for free online, but for our  use case it didn't support enough of the C standard.  So we added quite a number of features and functions.  Of course, a lot of these are not strictly required, for example, in its original use  case.  So, for example, the callbacks to extract information about program states and where  we are in the program, what functions are called, or also the non-deterministic types  and function support isn't necessarily part or doesn't need to be part of PicoC, but,  of course, it's required for our use case.  And to give you a bit of an overview about how NITWIT performs, we have collected the  results from the recent SVComp 2021.  Here you can see all the six validators that participated in SVComp 2021.  Blue means that a witness was successfully validated as a correct violation witness.  So these presented witnesses are only the violation witnesses.  And as you can see, for example, here NITWIT only shows blue and unknown or a timeout.  So we don't have the green color for true because NITWIT can never decide that a program  holds because it only explores a single state through the program.  So this is in stark contrast to, for example, CPA checker or ultimate automizer.  To give you a bit more information on how NITWIT performs, you can see time consumption  plotted over the witnesses.  So what you can see is basically that because we're using the interpreter approach, we have  a very, very low overhead for program start and setup, which you can see that, for example,  the next runner up in terms of startup time is the C-Prover witness to test program, also  called F-Shell, which is two orders of magnitude slower in initial startup and overhead than  NITWIT is.  Of course, C-Prover uses a similar approach to ours just that they use compilation in  the beginning.  So they first compile the program and then execute it instead of interpreting right  from the start.  And that's a trade-off because if you have a large program, the compiled program will  be a lot faster than the interpreter will ever be.  And you can clearly see that in how linearly it scales over larger programs, whereas NITWIT  starts taking up more time quickly with larger programs.  If we look at memory consumption, we can also see NITWIT has the advantage of the low overhead,  but of course, with larger programs, its memory consumption grows as well.  Here you can see an n-dimensional Venn diagram for coverage.  So this tells you which witnesses were covered by what tool.  We can see that, interestingly enough, there is something special for everyone.  So every tool has a couple of witnesses that only this tool really covers.  So every tool is a necessary and welcome addition to the pool.  At least that's what I would conclude from this.  Looking at the numbers, on the left you can see which verifier generated the witness and  then the columns tell you what tool could validate how many of these generated witnesses.  And one interesting takeaway I would say is that, of course, every tool is usually the  best verifier for its own witnesses.  So if you look at CPA checker, generated 1,293 witnesses, 1,327 witnesses, as seen in total  on the right, and CPA checker could validate 1,216, which is, of course, again a hint that  the witnesses are not always strong enough to really make the validation possible even  for the original tool.  And we can see a similar thing, for example, with Ultimate Automizer, which, as Marty and  Bolt could also verify the most witnesses of itself.  So to sum this up, we had a data set of 12,873 witnesses in total from REACH safety properties  in the recent SVCOM.  We could validate 8,100 of those successfully with NITWIT, which is the most under all participating  tools.  If we look at a bit of timing statistics, so for example, only on witnesses that were  successfully validated, we can see with the median time of 16 milliseconds, NITWIT is blazingly  fast.  If you look at the average, of course, it's a bit slower because of programs that get larger  and larger.  Remember the overhead tradeoff with the compilation.  If we look for comparison on all witnesses, so also those that we couldn't validate where  we, for example, ran into timeouts, which is, I guess, our biggest loss factor there,  you can see the median climbs slightly, but the average climbs a lot more.  And the same also applies for memory.  So in median, we only take about two megabytes, but of course, for the larger programs, you  can see in the standard deviation, we will take a lot more.  So in summary, our contribution is a new validator for violation witnesses called NITWIT.  It's available on GitHub.  It's open source and free.  It's quite fast.  It's independent of existing model checkers.  So if you don't trust them, you can use NITWIT.  It borrows semantics from your compiler.  So you can use different compilers to get an insight, for example, in differences between  compilers.  It supports 32 and 64-bit programs.  There's a lot more options available using compile time flags, and maybe in the future,  we will also implement witness refinement within NITWIT.  Thank you.
604907f51a80aac83ca25d83_0_59.png 604907f51a80aac83ca25d83_60_335.png 604907f51a80aac83ca25d83_336_1391.png 604907f51a80aac83ca25d83_1392_1607.png 604907f51a80aac83ca25d83_1608_3731.png 604907f51a80aac83ca25d83_3732_4631.png 604907f51a80aac83ca25d83_4632_5615.png 604907f51a80aac83ca25d83_5616_5855.png 604907f51a80aac83ca25d83_5856_6287.png 604907f51a80aac83ca25d83_6288_7619.png 604907f51a80aac83ca25d83_7620_9359.png 604907f51a80aac83ca25d83_9360_9923.png 604907f51a80aac83ca25d83_9924_11279.png 604907f51a80aac83ca25d83_11280_13451.png 604907f51a80aac83ca25d83_13452_14903.png 604907f51a80aac83ca25d83_14904_16535.png 604907f51a80aac83ca25d83_16536_16895.png 604907f51a80aac83ca25d83_16896_18059.png 604907f51a80aac83ca25d83_18060_20027.png 604907f51a80aac83ca25d83_20028_20399.png 604907f51a80aac83ca25d83_20400_21131.png 604907f51a80aac83ca25d83_21132_21863.png 604907f51a80aac83ca25d83_21864_22631.png 604907f51a80aac83ca25d83_22632_22883.png 604907f51a80aac83ca25d83_22884_22943.png 604907f51a80aac83ca25d83_22944_25007.png 604907f51a80aac83ca25d83_25008_26166.png