microsoft / infersharp

Infer# is an interprocedural and scalable static code analyzer for C#. Via the capabilities of Facebook's Infer, this tool detects null dereferences, resource leaks, and thread-safety violations. It also performs taint flow tracking to detect critical security vulnerabilities like SQL injections.
MIT License
727 stars 28 forks source link

Update Translation of Async for Resource Leak/Taint #214

Closed matjin closed 1 year ago

matjin commented 1 year ago

Async methods cause the compiler to spin up state machine classes around these methods; with new fields and methods. Particularly notably:

  1. Parameters of these async methods get stored in class fields in an initializer method
  2. The source code of this method gets put into a "MoveNext()" method within the state machine, along with some extra code.
  3. It seems that (at least sometimes) finally blocks are executed only if the value of a state field is >=0. This state field is supposed to be initialized to -1 by the initializer method. This was the root cause for observing false positives on iDisposable objects allocated via using within async methods.
  4. The return value of the method is instead set via a SetResult() method, as the MoveNext() method is actually void.

All of these technicalities are addressed in this PR, along with a QoL fix to a frequently encountered issue to do with wrong line numbers being reported, particularly for resource leaks. The changes are:

1/3 : We mock the initializer behavior: we inline Store instructions within the MoveNext() method which initialize the fields storing the parameters to the parameter values and initializes the state field to -1, so that Infer can correctly understand that the fields store the parameter values and that the state field is negative.

  1. We take the translation of the MoveNext() method and put the signature of the original method instead. This trick lets Infer apply the spec for the MoveNext() method containing the original source code whenever that method gets invoked (async method invocations look identical to how they would be if those methods were synchronous). We have to change the signature and change all ProgramVariables associated with all parameters and all return variables to be associated with the swapped method to ensure that Infer can track information flow properly.
  2. When we see a call to SetResult in a MoveNext() method, we instead treat this equivalently to a return instruction.

These changes generally enable Infer to treat the asynchronous methods almost identically to synchronous methods.

Additionally, the start node of a method is now mapped to the first real line of code, and the end node of a method is now mapped to the last real line of code. This should fix most of the issues we had encountered with line numbers.

Tested:

Added to the Examples.cs file some taint examples, focused on async methods, to validate the above changes. A false positive that had existed in the past with an async method returning an iDisposable method is now no longer reported, as desired.

xi-liu-ds commented 1 year ago

Latest Infer has skip-translation deprecated. I think we should update this line by replacing skip-translation as capture-block-list and removing language.

Please take a look at this example.

matjin commented 1 year ago

Latest Infer has skip-translation deprecated. I think we should update this line by replacing skip-translation as capture-block-list and removing language.

Please take a look at this example.

I removed the skip-translation. capture-block-list references Java/Clang specifically so not sure about compatibility with .NET. It looks nonessential anyway, so will delete for now.