{"id":42960,"date":"2022-10-31T09:05:00","date_gmt":"2022-10-31T16:05:00","guid":{"rendered":"https:\/\/devblogs.microsoft.com\/dotnet\/?p=42960"},"modified":"2022-10-27T16:05:26","modified_gmt":"2022-10-27T23:05:26","slug":"slaying-zombie-no-repo-crashes-with-infersharp","status":"publish","type":"post","link":"https:\/\/devblogs.microsoft.com\/dotnet\/slaying-zombie-no-repo-crashes-with-infersharp\/","title":{"rendered":"Slaying Zombie \u2018No Repro\u2019 Crashes with Infer#"},"content":{"rendered":"

You slide into your office chair, cup of coffee in hand, and check your email. Another high severity ticket \u2013 your servers have crashed, and you have by tomorrow morning to figure out why. Heaving a heavy sigh, you soon find yourself sifting through tens of thousands of lines of code and logs. Morning soon passes to afternoon, fading into dusk. Finally, you find it, push the fix, and reboot the application. Minutes pass. Crash<\/em>. Your night of the living dead has begun \u2013 no matter how many times you try to put this bug down, it just keeps coming back to life.<\/p>\n

We\u2019ve all suffered from \u201czombie bugs\u201d before. There are many static analysis tools on the marketplace today to help you detect bugs, many of which work by searching for a series of syntactic patterns in code. Unfortunately, due to the huge variation and complexity of coding constructs and conventions in different projects, this approach often leads to the high false positive and false negative rates for which static analysis tools are notorious. <\/p>\n

In today\u2019s post, we\u2019re going to show you how Infer#<\/a> can help you put down these zombie bugs, once and for all. Microsoft open-sourced Infer#<\/a> in 2020, which leverages Meta\u2019s Infer<\/a>. Infer# takes a different approach from other tools you\u2019ve heard of \u2013 it derives summaries of each method\u2019s semantics and reasons over the program\u2019s behavior. It uses incorrectness separation logic<\/a>, one of the latest advancements in program analysis research, to mathematically prove the presence of bugs in code. Infer# performs cross-assembly analysis to find issues like null pointer dereferences, resource leaks, and thread safety violations, in addition to security vulnerabilities like SQL injections and DLL injections.<\/p>\n

Getting started with Infer<\/h2>\n

With Infer# v1.4 you can identify security and performance issues with a single click, all in VS2022 and VSCode. First, make sure that Windows Subsystem for Linux (WSL)<\/a> is properly installed. Then, download and install the InferSharp extension from the Visual Studio<\/a> or Visual Studio Code<\/a> marketplaces. In this article, we\u2019ll show the VS experience, which is mimicked in VS Code. You can also use Infer# directly in WSL<\/a> and Docker<\/a>.<\/p>\n

The extension adds an Infer# Analysis<\/em> menu item to the Tools menu. The first time it\u2019s selected, it will complete setup by downloading and installing the Infer# custom WSL distro from Github. <\/p>\n

\"vs_menu_button\"<\/p>\n

Analyze your code<\/h2>\n

After waiting for setup to complete, selecting the Infer# Analysis<\/em> menu item again will prompt you to provide a directory tree (defaulting to the solution directory, if it exists) containing the DLLs and PDBs you want to analyze. Your selection is automatically saved for future runs in the .infersharpconfig<\/em> file created in your project directory. The analysis will then run, displaying the warnings in the Error List pane. Additionally, information about the analysis steps is shown in a pane on the right side of the editor, with clickable links to the relevant lines of code.<\/p>\n

\"analysis_steps\"<\/p>\n

Issue or not?<\/h2>\n

Now that we\u2019ve seen how to use Infer#, let\u2019s look at a couple of examples that demonstrate how Infer# works under the hood. Suppose we created the following IDisposable class OwnsStreamReader<\/code>:<\/p>\n

public class OwnsStreamReader : IDisposable\n{\n    public StreamReader reader;\n\n    public OwnsStreamReader(StreamReader input)\n    {\n        reader = input;\n    }\n\n    public void Dispose()\n    {\n        reader?.Dispose();\n    }<\/code><\/pre>\n
Does the following method contain a resource leak or not?<\/p>\n
    public static void LeakOrNot()\n    {\n        var fileStream = new FileStream(\"test.txt\", FileMode.Create, FileAccess.Write);\n        var reader = new StreamReader(fileStream);\n        using (var myClass = new OwnsStreamReader(reader))\n        {\n            myClass.reader.Read();\n        }\n    }<\/code><\/pre>\n
The answer is no<\/em>. Infer# determines this by producing method summaries that represent the semantics of OwnsStreamReader<\/code>\u2019s constructor and Dispose(). It determines that the Dispose() method takes care of the StreamReader, whose Dispose() in turn takes care of the FileStream object. The using statement ensures that the Dispose() function is invoked.<\/p>\n
Let\u2019s look at another example:<\/p>\n
    public class OwnsResources : IDisposable\n    {\n        private Socket socket;\n\n        private FileStream stream { get; set; } = new FileStream(\"test\", FileMode.Create);\n\n        public OwnsResources(SocketInformation info)\n        {\n            socket = new Socket(info);\n            stream = new FileStream(\"test\", FileMode.Create);\n        }\n\n        public void Dispose()\n        {\n            stream?.Dispose();\n            socket?.Dispose();\n        }<\/code><\/pre>\n
Is there a resource leak in the following method?<\/p>\n
        public static void LeakOrNot()\n        {\n            using (var myClass = new OwnsResources(new SocketInformation()))\n            {\n                myClass.stream.Flush();\n            }\n        }<\/code><\/pre>\n
The answer is yes<\/em>. Let\u2019s see what Infer# found:<\/p>\n
\"leak_or_not\"<\/p>\n
It reports \u201cResource dynamically allocated by constructor System.IO.FileStream(\u2026)is not closed after the last access at\u2026<\/em>\u201d The problem lies in the construction of the OwnsResources<\/code> class itself. The stream field gets initialized twice: once in its field initialization and again in the constructor. This is clear if we look at the bytecode, which is what Infer# uses to produce its analysis*:<\/p>\n
\"bytecode\"\n*You might notice that the first created object is stored into the stream field, whereas the second one is followed by an invocation of stream\u2019s setter method. A na\u00efve approach might not realize that these both have the ultimate effect of storing the object into the field. Infer#\u2019s semantic analysis of stream\u2019s setter method determines this equivalence.<\/p>\n
Removing one of the assignments and rerunning Infer# confirms that the issue is fixed:<\/p>\n
\"fixed\"<\/p>\n
Finding critical security issues in your code<\/h2>\n
Those of you building ASP.NET web apps might be familiar with issues like SQL injections<\/a> or using unsafe deserializers like BinaryFormatter<\/a>, which all involve the flow of information from an untrustworthy source into a sensitive location within the app. We\u2019re excited to announce the initial release of Infer#\u2019s ability to detect security vulnerabilities via taint analysis<\/em>. For example, suppose we have a project with the following method:<\/p>\n
namespace subproj\n{\n    public class WeatherForecast\n    {\n        public static void runSqlCommandBad(string input)\n        {\n            var command = new SqlCommand()\n            {\n                CommandText = \"SELECT ProductId FROM Products WHERE ProductName = '\" + input + \"'\",\n                CommandType = CommandType.Text\n            };\n            var reader = command.ExecuteReader();\n        }<\/code><\/pre>\n
On its own, this method doesn\u2019t pose a SQL injection issue, as it is only an issue if it gets invoked with a string input<\/code> that comes from a user-controlled source. An example of this would be the invocation of this method with input<\/code> coming as the parameter of a method with an HttpPost annotation. Infer# can detect this issue despite its trace spanning across multiple assemblies:<\/p>\n
\"taint\"<\/p>\n
Behind the scenes, Infer#\u2019 starts tracking tainted information when it passes through certain methods, known as \u201cpulse-taint-sources,\u201d specified in the ~\/infersharp\/.inferconfig<\/em> file in Infer#\u2019s WSL distro. This JSON specifies parameters to the analysis and is invoked by the extension by default. Infer# alerts when it detects that the tainted information reaches certain methods, known as \u201cpulse-taint-sinks.\u201d Putting it together, just specify the sources and sinks of the taint flow you want to track under \u201cpulse-taint-policies.\u201d Here\u2019s what that looks like for the case above:<\/p>\n
\"config\"<\/p>\n
You can easily specify more flows of your own, reusing sources and sinks as needed:<\/p>\n
\"more_flows\"<\/p>\n
Try it today!<\/h2>\n
By using a framework whose analysis stretches across all input assemblies, Infer# can detect issues that wouldn\u2019t be easy for a human to spot. We\u2019re excited to continue sharing with you the capabilities of the latest semantic analysis technologies. Become a zombie bug slayer today!<\/p>\n