Infer#: межпроцедурный анализ безопасности доступа к памяти для C#

Мы рады объявить о публичном выпуске Infer#, который предоставляет сообществу .NET возможности межпроцедурного статического анализа Infer. Кроме того, в рамках нашей приверженности открытому исходному коду проект был выпущен на GitHub под лицензией MIT.

Статический анализ — это метод, обычно используемый в рабочем процессе разработчика для проверки правильности исходного кода без необходимости его выполнения. Популярные анализаторы в экосистеме .NET — это FxCop и Roslyn. Infer# дополняет эти инструменты, обнаруживая межпроцедурные ошибки безопасности памяти, такие как разыменование null и утечки ресурсов.

Интегрируясь непосредственно в рабочий процесс разработчика для обнаружения ошибок надежности и безопасности перед их отправкой, Infer# поддерживает гибкую разработку для .NET. В самом деле, мы уже наблюдаем многообещающие первые результаты в отношении программного обеспечения Microsoft, такого как Roslyn, .NET SDK и ASP.NET Core.

Мы планируем и дальше расширять Infer#, и в будущем мы будем поддерживать безопасность потоков.

Подробнее под катом.

Межпроцедурный анализ валидации памяти для C#

Infer# в настоящее время обнаруживает нулевые разыменования (null dereferences) и утечки ресурсов. Мы проиллюстрируем каждую возможность ниже с ошибочным фрагментом кода вместе с соответствующим предупреждением, которое Infer# выводит об этом.

Чтобы узнать больше о технической реализации Infer#, посетите нашу вики.

Null Dereference

    static void Main(string[]) args)
    {
        var returnNull = ReturnNull();
        _ = returnNull.Value;
    }

    private static NullObj ReturnNull()
    {
        return null;
    }

internal class NullObj
{
    internal string Value { get; set; }
}

Переменной returnNull межпроцедурно присваивается значение null, а ссылка на нее разыменовывается посредством чтения поля Value. Это разыменование обнаружено:

/home/runner/work/infersharpaction/infersharpaction/Examples/NullDereference/Program.cs:11: error: NULL_DEREFERENCE (biabduction/Rearrange.ml:1622:55-62:)
  pointer 'returnNull' could be null and is dereferenced at line 11, column 13.

Утечка ресурсов

public StreamWriter AllocatedStreamWriter()
{
    FileStream fs = File.Create("everwhat.txt");
    return new StreamWriter(fs);
}

public void ResourceLeakBad()
{
    StreamWriter stream = AllocateStreamWriter();
    // FIXME: следует закрыть StreamWriter, вызвав stream.Close(), если stream не равен нулю.
}

Переменная Stream StreamWriter возвращается из AllocateStreamWriter, но не закрывается. Infer# сообщает об утечке ресурсов, что позволяет разработчику исправить ошибку:

/home/runner/work/infersharpaction/infersharpaction/Examples/ResourceLeak/Program.cs:11: error: RESOURCE_LEAK
  Leaked { %0 -> 1 } resource(s) at type(s) System.IO.StreamWriter.

Далее: нарушения безопасности потоков

Учитывая положительные отзывы, которые мы уже получили о способности Infer# обнаруживать нулевые разыменования и утечки ресурсов, мы работаем над дополнительными сценариями обнаружения дефектов. Нарушение безопасности потоков — это следующий сценарий на горизонте:

public class RaceCondition
{
    private readonly object __lockobj = new object();
    public int intField;
    public void WriteToField(int input)
    {
        lock (__lockObj)
        {
            intField = input;
        }
    }

    public int ReadFromField()
    {
        return intField;
    }
}

Хотя функция все еще находится в разработке, предупреждения будут появляться аналогично тому, как они появляются в Java; Блоки операторов lock() запускают анализ RacerD так же, как блоки Java synchronized().

/.../Examples/RaceCondition/Program.cs:39: error: THREAD_SAFTY_VIOLATION
  Read/Write race. Non-private method 'Int32 RaceCondition.ReadFromField()' reads without synchronization from 'this.intField'. Potentially races
with write in method 'RaceCondition.WriteToField(...)'.
  Reporting because another access to the same memory occurs on a background thread, although this access may not.

Пробуйте Infer#!