company_banner

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#!

    Microsoft
    Microsoft — мировой лидер в области ПО и ИТ-услуг

    Similar posts

    Comments 2

      +8
      Я не мог не оставить этот комментарий. :)
      Интересно находить ошибки с помощью инструмента поиска ошибок (PVS-Studio) в инструменте поиска ошибок (Infer#)… %)

      Предупреждение PVS-Studio: V3010 The return value of function 'Replace' is required to be utilized. MethodReferenceExtensions.cs 31

      Ссылка на код на GitHub.

      image

    Only users with full accounts can post comments. Log in, please.