pate
pate copied to clipboard
GaloisInc
Patches Assured up to Trace Equivalence
After we do an initial run of the verifier, we will have a differential summary that describes how the behavior of the program differs at an interesting program location. We...
Currently, errors in code discovery can be seen by manual inspection of individual slices (which contain the recovered macaw IR). It would be much more useful to make these errors...
There is now a gas parameter to force termination, but there have been cases that tickle non-termination that we really should investigate. It should in principle terminate, so the fact...
Currently, our precise memory model is quite slow. It's possible that one reason for this is that it needs to check quite a lot of sanity conditions on every read...
The new memory model is slow slow slow. We think one possible reason is its use of symbolic structs -- we always know concretely what field we want, so symbolic...
When reading from memory, the new memory model currently reassembles bytes by shifting and masking. If we use bitvector concatenation instead, that will more clearly indicate our intent -- and...
As the proof and counter-example types become more complicated and further abstracted from the types used by the verifier, the conversion between these types becomes nontrivial. This warrants a diagram...
It is getting a bit crowded. Separate modules for at least the command line options, the hint parsing code, and the terminal logger would help a great deal.
Some potential users of our tool would find it very useful to be able to consume the function-level pre- and post-domain information we are generating. We need to export this...
Currently loops that cannot be statically unrolled will result in the symbolic execution stage simply hanging indefinitely. To handle this, we need to explicitly slice loops out of the CFG...