Is static analysis really formal verification?

Question

I have been reading about formal verification and the basic point is that it requires a formal specification and model to work with. However, many sources classify static analysis as a formal verification technique, some mention abstract intepretation and mention its use in compilers. So I am confused - how can these be formal verification if there is no formal description of the model?
EDIT: A source I found reads:

Static analysis: the abstract semantics is computed automatically from the program text according to predefined abstractions (that can sometimes be tailored automatically/manually by the user)

So does it mean it works just on the source code with no need for formal specification? This would be what static analysers do.

Also, is static analysis possible without formal verification? E.g. does SonarQube really perform formal methods?

Answer 1

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

How can these be formal verification if there is no formal description of the model?

A static analyser will generate control/data flow of a piece of code, upon which formal methods can then be applied to verify conformance to the system's/unit's expected design model.

Note that modelling/formal-specification is NOT a part of static-analysis.
However combined together, both of these tools are useful in formal verification.

---

For example if a system is modeled as a Finite State Machine (FSM) with

• a pre-defined number of states
  defined by a combination of specific values of certain member data.
• a pre-defined set of transitions between various states
  defined by the list of member functions.

Then the results of static analysis will help in formal verification of the fact that
the control NEVER flows along a path that is NOT present in the above FSM model.

Also, if a model can be simply defined in terms of type-definition, data-flow, control-flow/call-graph, i.e. code-metrics that a static-analyser can verify, then static-analysis itself is sufficient to formally verify that code conforms to such a model.

_{NOTE1. The yellow region above would be static analysers used to enforce stuff like coding-guidelines and naming-conventions i.e. aspects of code that cannot affect the program's behavior.}

_{NOTE2. The red region above would be formal verification that requires additional steps like 100% dynamic code-coverage, elimination of unused and dead code. These cannot be detected/enforced using a static-analyser.}

---

Static analysis is highly effective in verifying that a system/unit is implemented using a subset of the language specification to meet goals laid out in the system/unit design.

For example, if it is a design goal to prevent the stack memory from exceeding a particular limit, then one could apply a limit on the depth of recursion (or forbid recursive functions calls altogether). Static-analysis is used to identify such violations of design goals.

In the absence of any warnings from the static-analyser,
the system/unit code stands formally verified against such design-goals of its respective model.

eg. MISRA-C standard for Automotive software defines a subset of C for use in automotive systems.

MISRA-C:2012 contains

• 143 rules - each of which is checkable using static program analysis.

• 16 "directives" more open to interpretation, or relate to process.

Answer 2

Static analysis just means "read the source code and possibly complain". (Contrast to "dynamic analysis", meaning, "run the program and possibly complain about some execution behavior").

There are lots of different types of possible static-analysis complaints. One possible complaint might be,

 Your source code does not provably satisfy a formal specification

This complaint would be based on formal verification if the static analyzer had a formal specification which it interpreted "formally", a formal interpretation of the source code, and a trusted theorem prover that could not find an appropriate theorem.

All the other kinds of complaints you might get from a static analyzer are pretty much heuristic opinions, that is, they are based on some informal interpretation of the code (or specification if it indeed even exists).

The "heavy duty" static analyzers such as Coverity etc. have pretty good program models, but they don't tell you that your code meets a specification (they don't even look to see if you have one). At best they only tell you that your code does something undefined according to the language ("dereference a null pointer") and even that complaint isn't always right.

So-called "style checkers" such as MISRA are also static analyzers, but their complaints are essentially "You used a construct that some committee decided was bad form". That's not actually a bug, it is pure opinion.