Техники за анализ на статичен код при откриване на целочислени препълвания

Може да си струва да опитате с cppcheck инструмент за статичен анализ, който искове за откриване на целочислено препълване със знак от версия 1.67:

Нови проверки:
- Открива преместване с твърде много битове, препълване на цели числа със знак и опасно преобразуване на знаци

Забележете, че поддържа както C, така и C++ езиците.

Няма проверка за препълване за цели числа без знак, тъй като стандартните типове без знак никога не препълват.

Ето някои основни примери:

#include <stdio.h>

int main(void)
{
    int a = 2147483647;
    a = a + 1;

    printf("%d\n", a);

    return 0;
}

С такъв код се получава:

$ ./cppcheck --platform=unix64 simple.c 
Checking simple.c...
[simple.c:6]: (error) Signed integer overflow for expression 'a+1'

Въпреки това не бих очаквал твърде много от него (поне с текущата версия), тъй като програмата е малко по-различна:

int a = 2147483647;
a++;

минава без да забележи преливане.

Изглежда, че търсите някакъв вид анализ на диапазона на стойността и откривате кога този диапазон би надхвърлил зададените граници. Това е нещо, което на пръв поглед изглежда просто, но всъщност е трудно. Ще има много фалшиви положителни резултати и това е дори без да се броят грешките в изпълнението.

За да пренебрегнете подробностите за момент, вие свързвате двойка [lower bound, upper bound] с всяка променлива и правите малко математика, за да разберете новите граници за всеки оператор. Например, ако кодът добави две променливи, във вашия анализ добавяте горните граници заедно, за да образувате новата горна граница, и добавяте долните граници заедно, за да получите новата долна граница.

Но разбира се не е толкова просто. Първо, какво ще стане, ако има код, който не е прав? if не са много лоши, можете просто да оцените и двете страни и след това да вземете обединението на диапазоните след него (което може да загуби информация! ако два диапазона имат празнина между тях, тяхното обединение ще обхване празнината). Циклите изискват трикове, една наивна реализация може да изпълни милиарди итерации на анализ на цикъл или дори никога да не приключи. Дори ако използвате абстрактен домейн, който няма безкрайни възходящи вериги, пак можете да си навлечете проблеми. Ключовите думи за решаване на това са "оператор за разширяване" и (по избор, но вероятно е добра идея) "оператор за стесняване".

Още по-лошо е от това, защото какво е променлива? Вашата обикновена локална променлива от скаларен тип, която никога не получава адреса си, не е много лоша. Но какво да кажем за масивите? Сега дори не знаете със сигурност кой запис е засегнат - самият индекс може да е диапазон! И тогава има псевдоним. Това далеч не е решен проблем и кара много инструменти от реалния свят да правят наистина песимистични предположения.

Също така, извиквания на функции. Ще извикате функции от някакъв контекст, надяваме се известен (ако не, тогава е просто: не знаете нищо). Това го затруднява, не само внезапно има много повече състояние, което да се следи едновременно, може да има няколко места, от които може да бъде извикана функция, включително самата. Обичайният отговор на това е да се преоцени тази функция, когато диапазон от един от нейните аргументи е бил разширен, още веднъж това може да отнеме милиарди стъпки, ако не се направи внимателно. Има и алгоритми, които анализират функция по различен начин за различен контекст, което може да даде по-точни резултати, но е лесно да отделите много време за анализиране на контексти, които не са достатъчно различни, за да имат значение.

Както и да е, ако сте стигнали дотук, можете да прочетете Accurate Static Предсказване на клонове чрез разпространение на диапазон на стойност и свързани документи, за да получите добра представа как всъщност да направите това.

И това не е всичко. Разглеждането само на обхватите на индивидуалните променливи, без да се интересува от връзките между тях (ключова дума: нерелационна абстрактна област), се отразява лошо на наистина прости (за човешки читател) неща като изваждане на две променливи, които винаги са близки една до друга по стойност, за което ще направи голям диапазон, като се допуска, че те могат да бъдат толкова далеч един от друг, колкото границите им позволяват. Дори за нещо тривиално като напр

; assume x in [0 .. 10]
int y = x + 2;
int diff = y - x;

За човешкия читател е доста очевидно, че diff = 2. В анализа, описан дотук, заключенията биха били, че y in [2 .. 12] и diff in [-8, 12]. Сега да предположим, че кодът продължава с

int foo = diff + 2;
int bar = foo - diff;

Сега получаваме foo in [-6, 14] и bar in [-18, 22], въпреки че bar очевидно отново е 2, диапазонът отново се удвои. Това беше прост пример и можете да измислите някои ad hoc хакове, за да го откриете, но това е по-общ проблем. Този ефект има тенденция бързо да раздува обхватите на променливите и да генерира много ненужни предупреждения. Частично решение е присвояването на диапазони на разликите между променливите, след което получавате това, което се нарича обвързана с разликата матрица (не е изненадващо, че това е пример за релационна абстрактна област). Те могат да станат големи и бавни за междупроцедурен анализ или ако искате да им хвърлите и нескаларни променливи, и алгоритмите започват да стават по-сложни. И ви стигат само дотук - ако добавите умножение към сместа (която включва x + x и варианти), нещата пак се влошават много бързо.

Така че можете да добавите нещо друго в микса, което може да се справи с умножението по константа, вижте например Абстрактни области на афинни релации⋆ - това е много различно от диапазоните и само по себе си няма да ви каже много за диапазоните на вашите променливи, но можете да го използвате, за да получите по-точни диапазони.

Историята не свършва дотук, но този отговор става дълъг. Надявам се, че това не ви обезсърчава да проучвате тази тема, това е тема, която се поддава добре, за да започнете просто и да добавите все повече и повече интересни неща към вашия инструмент за анализ.

Проверка на целочислени препълвания в C:

Когато добавите две 32-битови числа и получите 33-битов резултат, по-малките 32 бита се записват в дестинацията, като най-високият бит се сигнализира като флаг за пренасяне. Много езици, включително C, не предоставят начин за достъп до това „пренасяне“, така че можете да използвате ограничения, т.е. <limits.h>, за проверка, преди да извършите аритметична операция. Помислете за unsigned ints a и b :

ако MAX - b < a, знаем със сигурност, че a + b ще причини препълване. Пример е даден в този ЧЗВ за C.

Внимавайте: Както chux посочи, този пример е проблематичен с цели числа със знак, защото няма да обработи MAX - b или MIN + b, ако b < 0. Примерното решение във втората връзка (по-долу) обхваща всички случаи.

Умножаването на числа също може да причини препълване. Решението е да удвоите дължината на първото число, след което да извършите умножението. Нещо като:

(typecast)a*b  

Внимавайте: (typecast)(a*b) би било неправилно, защото първо съкращава, а след това преобразува.

Подробна техника за c можете да намерите ТУК. Използването на макроси изглежда лесно и елегантно решение.

Очаквам Frama-C да предостави такава възможност. Frama-C е фокусиран върху изходния код на C, но не знам дали е чувствителен към диалект или специфичен. Вярвам, че използва абстрактна интерпретация за моделиране на стойности. Не знам дали специално проверява за препълване.

Нашият DMS Software Reengineering Toolkit има разнообразие от предни части на езика, включително повечето основни диалекти на C. Предоставя контрол и анализ на потока от данни, както и абстрактна интерпретация за изчислителни диапазони, като основи, върху които можете да изградите отговор. Моят Google Tech Talk относно DMS около 0:28:30 конкретно говори за това как човек може да използва абстрактната интерпретация на DMS за диапазони от стойности, за да открие препълване (на индекс в буфер). Вариант на проверката на горната граница на размерите на масива е просто да се провери за стойности, които не надвишават 2^N. Готовият DMS обаче не предоставя никакъв специфичен анализ на препълване за C код. Има място за ОП да върши интересна работа :=}