SAL. Контрактне програмування від Мікрософт або як допомогти статичного аналізатора

Мова анотації вихідного коду (SAL).
По моєму це тема незаслужено обійдена увагою: не надено жодної згадки в рунеті.
Сам собі не допоможеш ніякої статичний аналізатор тобі не допоможе.

Стаття буде цікава програмістам не довіряють собі і оточуючим.
Людям, які використовують статичний аналізатор або збираються використовувати.

Передісторія

.
POS термінал. 50тис. рядків. 10 років історії. Чистий 'C', який не знав сучасних компіляторів. І Я весь в білому.
Перш ніж на щось вступити необхідно забезпечити тили:
1. Зачистка попереджень, наскільки це можливо.
2. Аналіз коду статичними аналізаторами (MSVC2010, PVS-Studio, MSVC2013).

Це принесло користь, але можливості статичних аналізаторів обмежені, на ЖАЛЬ.
Проста обгортка над memcpy зводить нанівець потуги аналізаторів, а про унікальних невідомо-чого скільки приймають-відправляють функцій і говорити не доводиться.
Мені потрібні статичні ГАРАНТІЇ (помріяти то можна) безпеки коду.

І тоді я зацікавився: чи можна використовувати макроси із стандартної бібліотеки Мікрософт.

void * memcpy(
_Out_writes_bytes_all_(count) void *dest, 
_In_reads_bytes_(count) const void *src, 
size_t count
);

Виявилося можна і навіть потрібно.

Навіщо

Мова анотації вихідного коду (SAL) дозволяє вказати аналізатору допустимі значення вхідних-вихідних парметр. Після чого аналізатор повідомить про потенційні порушення безпеки.

Найпростіший приклад містить 2 помилки і ліки:

// шкідлива функція 
void func (_Out_writes_z_(9) char * str)
{
strcpy(str, "20141201XXXXXX");
}
void main()
{
char str[5];
// небезпечне використання
func (str);
}


Використання

Використання дуже банально.
Довідка Мікрософт містить вичерпні відомості з даного питання: msdn.microsoft.com/ru-ru/library/hh916382.aspx
#include <sal.h>
містить короткий посібник з використання.

Дуже коротко, макроси:

  1. _In_ посилання на входно параметр
  2. _Out_ посилання на вихідний параметр
  3. _In_z_ рядок закінчується нулем
  4. _In_reads_(s) масив елементів
  5. _Out_writes_z_(s) масив розміру «s» для рядка заканчивающеся нулем
І так далі.

Заголовок спойлера
void func( 
_In_ int * v1, 
_In_z_ char * s, 
_In_reads_(m_len) char * m, 
int m_len, 
_Out_writes_z_(so), int so_len)
{
*v1;
strlen(s);
m[m_len - 1];
strncpy(so, so_len, " 234234234");
}




Мінуси

  • Мікрософт специфіка.
  • Існують 2 версії мови
  • Intellisense QtCreator-а не сприймає макросів в оголошеннях функцій
  • Оголошення стають витонченими


Ще один інструмент боротьби.

Джерело: Хабрахабр

0 коментарів

Тільки зареєстровані та авторизовані користувачі можуть залишати коментарі.