In terms of tools, slither & mythril are the ones most widely used. However, most of the tools out there will only identify a set of generic issues that are independent of the contract logic and business rules. It is worth noting that most of these tools will report a significant amount of false positives (as one does more audits, it gets easier and faster to spot them). In summary, tools will only get you basic findings. The true value of an audit is the experience brought by the audit team. And yes, the audit team will need to read the code line by line…
The learning path to be an auditor is not necessarily a straight road and I am unaware there is even one generic program (proprietary or not). In all truthfulness, I believe auditing is something you learn by doing once you have mastered the security best practices concerning smart contract development.
Essentially, any auditing process should do two things:
- Given a specification (e.g., white paper, internal docs, external docs), verify that the code is doing what the specifications is stating. The goal here is to check whether the code is in tune with the business requirements. This is an intensive and very tedious task. You essentially read the code, understand it, and make sure it meets the given specification.
- From the previous step, you should have been able to get a mental model of the entire platform that you are auditing. Then, you start investigating more insightful things, and how one could put the pieces together in a way that developers had not thought of. Here you need to have (or develop) an attacker mindset and this experience comes with time. A good way to bootstrap that mindset is to read postmortems and replay the attack yourself. Having built a mental model of the code you are auditing, you start investigating potential threats, by means of asking questions like:
- Is it possible for any actor to put the contract in an unusable state?
- Is there a sequence of transactions that could cause the smart contract to misbehave?
- Are funds secure?
- Are there underlying assumptions made by the contract that may not hold?
- Are there interactions with external contracts? If so, are they trusted? If not, how could they exploit the current code?
- etc.
Let me know if that helps. I am happy to provide more hints as you keep directing me :)