정적 드라이버 검증 도구 일반 도구 및 기술 제한 사항

아티클
06/15/2023

SDV에는 다음과 같은 일반적인 제한 사항이 있습니다.

SDV는 한 번에 하나의 드라이버만 확인하고 드라이버는 WDM, KMDF, NDIS 또는 Storport와 같은 드라이버 모델 중 하나를 따라야 합니다. 지원되는 드라이버에 대한 자세한 내용은 정적 드라이버 검증 도구가 드라이버 또는 라이브러리를 지원하는지 여부를 확인합니다.
위의 범주 중 하나에 속하지 않는 드라이버는 확인할 수 있고 분석 중에 실패할 가능성이 높은 규칙에서 심각하게 제한됩니다.
드라이버 프로젝트 파일 및 소스 코드는 로컬 컴퓨터에 있어야 합니다. 드라이버를 원격으로 확인할 수 없습니다.
SDV는 영어(미국) 로캘과 함께 설치됩니다. 따라서 문자열 서식 지정과 같은 로캘 종속 요소는 영어(미국) 변형을 사용합니다. 이 제한은 SDV가 영어(미국) 이외의 지역화된 Windows 버전에 설치된 경우에도 존재합니다.

SDV 확인 엔진 에는 일부 드라이버 코드를 올바르게 해석하지 못하도록 하는 기술적 제한 사항이 있습니다. 특히 확인 엔진은 다음과 같습니다.

32비트 정수는 32비트로 제한된다는 것을 인식하지 못합니다. 따라서 오버플로 또는 언더플로 오류를 검색하지 않습니다.
정적 키워드(keyword) 사용하여 진입점을 선언하는 드라이버가 올바르게 처리되었는지 확인합니다. 그러나 정적 진입점을 인식하려면 SDV에서 정적 함수에 대한 Sdv-map.h 파일을 변경해야 했습니다. 예를 들어 정적 진입점을 선언하는 경우:
```
static DRIVER_UNLOAD Unload;
```
Sdv-map.h에는 fun_DriverUnload 대한 일반적인 항목이 포함되지 않습니다.
```
#define fun_DriverUnload Unload
```
대신 함수 이름이 망가진 것을 볼 수 있습니다.
```
  #define fun_DriverUnload sdv_static_function_Unload_1
```
여러 모듈에 Unload라는 정적 함수가 있을 수 있으므로 이 작업이 필요합니다. 잠재적 충돌을 방지하기 위해 이름이 손상되었습니다.
내보내기 드라이버에 드라이버 디스패치 함수를 숨기는 모듈 정의(.def) 파일이 있는 내보내기 드라이버에 정의된 드라이버 디스패치 또는 드라이버 콜백 함수를 해석할 수 없습니다. 이 문제를 방지하려면 모듈 정의(.def) 파일의 EXPORTS 섹션에 드라이버 디스패치 함수를 추가합니다.
이 함수에 대한 다음 참조가 동일한 컴파일 단위에 없는 경우 함수의 역할 유형을 성공적으로 검색할 수 없습니다.
- 함수의 선언입니다.
- 함수의 정의입니다.
- 드라이버 진입점 또는 콜백 함수에 함수를 할당합니다.
컴파일 단위는 이 소스 코드 파일에 포함된 가장 작은 소스 코드 파일 및 기타 소스 파일 집합으로 정의됩니다.

SDV에서 함수 역할 형식을 검색하지 않으면 SDV는 이 함수에서 시작된 추적을 확인하지 않습니다.

예를 들어 드라이버가 mydriver.c 파일에서 EvtDriverDeviceAdd 함수를 정의(또는 구현)하는 경우입니다. 이 컴파일 단위(또는 mydriver.c에 포함된 모든 .h 파일)에는 EvtDriverDeviceAdd 함수에 대한 함수 역할 형식 선언이 포함되어야 합니다.
구조적 예외 처리를 해석하지 않습니다. try/except 문의 경우 SDV는 예외가 throw되지 않은 것처럼 보호된 섹션을 분석합니다. 식 또는 예외 처리기 코드를 분석하지 않습니다.
```
// The try/except statement
__try 
{
   // guarded section
}
__except ( expression )
{
   // exception handler
} 
```
try/finally 문의 경우 SDV는 예외가 throw되지 않은 것처럼 보호된 섹션과 종료 처리기를 분석합니다.
```
// The try/finally statement
__try {
   // guarded section
}
__finally {
   // termination handler
}
```
try/except 및 try/finally 문 모두에 대해 SDV는 leave 문을 무시합니다.

try/except 및 try/finally 문 모두에 대해 try 블록에서 점프하면 예외 또는 finally 문을 분석할 수 없습니다. leave 문을 사용할 수 있도록 다시 작성하는 방법에 대한 자세한 내용은 컴파일러 경고 C6242에 대한 항목을 참조하세요.
포인터 산술을 무시합니다. 예를 들어 포인터가 증가하거나 감소하는 상황이 누락됩니다. 이 제한으로 인해 가음성 및 가양성 결과가 발생할 수 있습니다.
공용 구조체를 무시합니다. 대부분의 경우 공용 구조체는 구조체로 처리되며 이로 인해 가양성 또는 거짓 부정이 발생할 수 있습니다.
캐스팅 작업을 무시하므로 다시 캐스팅으로 해결된 오류와 캐스팅으로 인해 발생하는 오류가 모두 누락됩니다. 예를 들어 엔진은 문자로 다시 캐스팅되는 정수에 여전히 정수 값이 있다고 가정합니다.
함수 포인터 배열인 배열만 초기화합니다. SDV는 경고를 실행하고 배열 이니셜라이저를 처음 1000개 요소로 압축합니다. 다른 배열 형식의 경우 첫 번째 요소만 초기화됩니다.
배열에서 초기화된 개체의 생성자는 호출되지 않습니다. 예를 들어 다음 코드 조각에서는 SDV 가 생성자를 호출하지 않으므로 x가 10으로 설정되지 않습니다.
```
class A
{
public:
    A() {
      x = 10;
    }

    int x;
};

void main()
{
    A a[1];
}
```
SDV는 배열을 초기화하는 생성자 사용을 지원하지 않습니다. 예를 들어 다음 코드 조각에서 P에 대한 생성자는 기본 함수에서 올바르게 호출되지 않으며 배열 p2에서 요소를 초기화하지 않습니다.
```
class P
{
public:
    P() : x(0) {}
    int x;
};

void main()
{
    P* p1 = new P[1];

    P p2[1] = {P()};
}
```
SDV는 미리 컴파일된 헤더를 무시합니다. 컴파일 속도를 높이기 위해서만 미리 컴파일된 헤더를 사용하는 드라이버는 SDV를 사용하여 더 느리게 컴파일됩니다. 컴파일에 성공하기 위해 미리 컴파일된 헤더를 사용해야 하는 드라이버는 SDV로 컴파일되지 않습니다.
RtlZeroMemory 또는 NdisZeroMemory 호출을 통해 수행되는 일부 유형의 암시적 할당을 유추할 수 없습니다. 엔진은 메모리를 0으로 초기화하기 위해 최선의 분석을 수행하지만 형식을 식별할 수 있는 경우에만 수행합니다. 따라서 메모리를 초기화하기 위해 이러한 함수에 의존하는 코드는 일부 코드 경로를 따라 잘못된 결함을 초래할 수 있습니다.
KMDF 드라이버에 대한 I/O 요청의 수동 디스패치를 추적할 수 있는 메모리 모델을 지원하지 않습니다. 엔진은 I/O 요청을 드라이버에 전달하기 위해 프레임워크를 사용하는 메서드만 지원합니다(순차적 또는 병렬 디스패치용).
비교를 위해 float 데이터 형식의 사용을 지원하지 않습니다. 이러한 기술적 제한으로 인해 가음성 및 가양성 결과가 발생할 수 있습니다.
SDV는 가상 상속 또는 가상 함수를 지원하지 않습니다. SDV는 가상 함수를 통해 코드 경로를 따르는 결함을 생성하지 않으므로 실제 결함이 손실될 수 있습니다. 가상 상속은 일반 상속처럼 처리되며, 이로 인해 잘못된 결함이 있거나 실제 결함이 손실될 수 있습니다.

다음을 통해 공유

정적 드라이버 검증 도구 일반 도구 및 기술 제한 사항

피드백

추가 리소스