ecrecover related bugs are not detected about pakala HOT 7 CLOSED

Yes, ecrecover() is not hard to do if the "concrete" cases. It's much harder when you give it symbolic things, but we could at least try to concretize them and try a few values (I already do that in a few other places).
Mostly I need to take a look at it and implement it, and also have a clean way to plug precompiles… It requires some time to implement properly, even if it's not too hard to support the easy concrete cases.

from pakala.

Hi,

Thanks for your interest in Pakala. Yes, I don't implement support for precompiles yet.

Overall, the support for calling external contracts is very limited in Pakala, and that also includes precompiles for now. I will try to make this clearer in the documentation.

I'm gonna leave this issue open. Some precompile could probably be implemented easily.

from pakala.

I clarified the readme. I may try to implement support for ecrecover(), but it has a pretty low priority in my TODO list though.

from pakala.

I have a few thoughts on this, I hope you don't mine me dumping them here, it's a really interesting tool which does a few things which others don't - although, others do a few things that Pakala doesn't etc. For example, you took an approach with the SHA3 builtin which others hadn't considered - symbolic analysis of the inputs to a hash function etc.

To support precompiles I guess this depends on two things:

1. knowing all of the possible values of an item in the stack, so you can determine that the CALL address is a precompile (which should be really easy when you push a constant onto the stack).
2. For ecrecover - having two code paths, one where the output area of memory is unchanged (e.g. an invalid signature), and one where it's the truncated result of a hash of a public key (e.g. the Ethereum address)

Another thing to consider is, say if you're doing input tracing, and you're comparing the result of a signature (where you control all the parameters) with an address that you also provide as input - surely this kind of thing should be detected? e.g. controlling all inputs, and the expected output, which is used as the condition for some code path, means that path must be accessible.

from pakala.

One thing that really bugs me about symbolic analysis of ethereum contracts, is that most tools - including yours - when they can't reason about a contract or if it's too complex - they exit successfully.

If you are trying to formally verify that your contract is not exploitable, if you run all of the tools on it and none of them find any problem, it doesn't mean that your contract has no exploits...

But, a different way is, if you cannot fully and 100% reason about the impossibility of a smart contract being exploited, then you should return 'POSSIBLY VULNERABLE', right?

It's 100% possible to have a subset of solidity and EVM assembly which is formally verifiable, where you can guarantee that there are no exploits, I think this is of more value to the Ethereum ecosystem than something which gives you the false impression of being secure just because 'nothing found anything', right?

We would really love to be able to say with certainty, that a contract is secure, rather than saying "we don't know about any exploits for the contract" etc

from pakala.

As an add-on to that:

With Pakala, I think it's possible that we could have an ERC-20 contract which is formally verifiably secure. It i

from pakala.

There are a few metrics like coverage and the warning about forced concretization that will tell you whether it could analyze the contract deeply or not.
Pakala was not made to formally verify or do a sound analysis. As in the description, it's an offensive analysis tool.

If you want a tool that you describe, you need a sound analysis. For that you have to look at formal verification, or tools like https://github.com/NASA-SW-VnV/ikos (not for ethereum, just for the sake of the example).

from pakala.