장치 드라이버 통합 및 검증

Device driver synthesis and verification
The Device Driver architecture.
장치 드라이버.

장치 드라이버는 소프트웨어 또는 상위 수준의 컴퓨터 프로그램이 하드웨어 장치와 상호 작용할 수 있도록 하는 프로그램이다.이러한 소프트웨어 구성요소는 이러한 각 시스템과 통신하고 명령을 실행하면서 장치와 운영체제 사이의 연결고리 역할을 한다.그들은 위의 소프트웨어에 추상화 계층을 제공하고 또한 운영 체제 커널과 아래의 장치들 사이의 통신을 중재한다.

일반적으로 운영체제는 공통 장치 드라이버에 대한 지원을 제공하며, 대개 하드웨어 공급업체는 대부분의 플랫폼용 하드웨어 장치에 대한 장치 드라이버를 제공한다.하드웨어 장치와 복잡한 소프트웨어 구성요소의 공격적인 확장은 장치 드라이버 개발 프로세스를 번거롭고 복잡하게 만들었다.드라이버의 크기와 기능이 증가하기 시작했을 때 장치 드라이버는 시스템의 신뢰성을 정의하는 핵심 요소가 되었다.이것은 기기 드라이버의 자동 합성과 검증에 대한 동기를 만들었다.본 문서는 기기 드라이버의 종합과 검증에서 일부 접근방식을 조명한다.

자동 운전자 통합 및 검증의 동기

장치 드라이버는 대부분의 시스템에서 주요 고장 부품이다.BOINC(Berkeley Open Infrastructure for Network Computing) 프로젝트는 OS 충돌이 주로 서툰 장치 드라이버 코드에 의해 발생한다는 것을 발견했다.[1]Windows XP에서 드라이버는 보고된 고장의 85%를 차지한다.Linux 커널 2.4.1에서 장치 드라이버 코드는 코드 크기의 약 70%를 차지한다.[2]드라이버 결함은 커널 모드에서 실행 중인 시스템 전체를 충돌시킬 수 있다.이러한 결과는 기기 드라이버의 검증을 위한 다양한 방법론과 기법을 도출했다.대안은 장치 드라이버를 견고하게 합성할 수 있는 기술을 개발하는 것이었다.개발 프로세스에서 인적 상호작용이 적고 기기 및 운영체제의 적절한 사양이 더 신뢰할 수 있는 드라이버로 이어질 수 있다.

운전자 합성을 위한 또 다른 동기는 많은 수의 운영 체제와 기기 조합이다.이들 각각은 각각의 운영체제에서 하드웨어 장치의 지원을 어렵게 하는 고유의 입출력 제어장치와 사양을 가지고 있다.따라서 운영 체제에서 장치를 사용할 수 있는 능력은 해당 장치 드라이버 조합의 가용성을 요구한다.하드웨어 공급업체는 대개 Windows, Linux, Mac OS용 드라이버를 공급하지만 개발 또는 포팅 비용이 높고 기술 지원이 어려워 모든 플랫폼에서 드라이버를 제공할 수 없다.자동화된 합성 기법은 어떤 운영체제에서든 어떤 장치를 지원하는 드라이버를 공급하는데 공급업체가 도움을 줄 수 있다.

장치 드라이버 확인

장치 드라이버의 테스트를 제한하는 두 가지 과제가 있다.

  • 드라이버와 커널의 상호 작용에 결함이 있을 때 정확한 작동이나 시간을 결정하는 것은 매우 어렵다.시스템이 일정하지 않은 상태로 전환될 수 있고, 오랜 시간이 흐른 후에 추락이 보고되어 실제 사고 원인이 흐려질 수 있다.
  • 정상적인 상황에서 제대로 작동하는 운전자는 드물고 예외적인 경우에 잘못될 수 있으며 전통적인 시험 기법은 운전자의 코너 케이스 행동을 탐지하는 데 도움이 되지 않을 수 있다.

기기 드라이버 검증의 물결은 마이크로소프트가 2000년 초 SLAM 프로젝트를 통해 시작되었다.이 프로젝트의 동기는 하루 50만 건의 추락사고가 한 명의 영상 드라이버에 의해 발생하는 것으로 밝혀져 복잡한 기기 드라이버 사용 시 큰 취약성을 우려하게 되었다.더 자세한 내용은 빌 게이츠가 행한 연설에서 찾을 수 있다.이후 버그 검출과 격리를 위해 다수의 정적 및 런타임 기법이 제안되었다.

정적 분석

정적 분석이란 프로그램을 분석하여 지정된 안전 중요 속성에 부합하는지 여부를 확인하는 것을 말한다.예를 들어 시스템 소프트웨어는 "커널 데이터 구조에 쓰기 전에 사용자 권한 확인", "확인 없이 null 포인터를 참조하지 마십시오", "버퍼 크기 초과 방지" 등의 규칙을 준수해야 한다.실제로 확인 중인 코드를 실행하지 않고도 이러한 검사를 수행할 수 있다.전통적인 테스트 프로세스(동적 실행)를 사용하려면 이러한 경로를 실행하고 시스템을 오류 상태로 만들기 위해 많은 테스트 사례를 작성해야 한다.이 과정은 오랜 시간과 노력이 들 수 있고 실질적인 해결책이 아니다.이론적으로 가능한 또 다른 접근방식은 수작업 검사지만, 이것은 수백만줄의 코드가 관여하는 현대 시스템에서는 비실용적이기 때문에 논리가 너무 복잡해서 인간이 분석할 수 없다.

컴파일러 기법

소스 코드에 대한 직접 매핑이 있는 규칙은 컴파일러를 사용하여 확인할 수 있다.규칙 위반은 소스 작업이 이치에 맞지 않는지 확인하여 찾을 수 있다.예를 들어 기능 호출 순서를 보면 "사용 불가능 후 인터럽트 활성화"와 같은 규칙을 확인할 수 있다.그러나 소스 코드 유형 시스템이 의미론에서 규칙을 지정할 수 없다면 컴파일러는 그러한 종류의 오류를 포착할 수 없다.많은 타입 세이프 언어는 안전하지 않은 타입 캐스팅으로 인한 메모리 안전 위반을 컴파일러에 의해 탐지할 수 있게 한다.

또 다른 접근방식은 메타 레벨 컴파일(MC)을 사용하는 것이다.[3]이러한 목적을 위해 제작된 메타콤필러는 경량 시스템별 체커 및 최적화 도구로 컴파일러를 확장할 수 있다.이러한 확장자는 시스템 구현자가 높은 수준의 언어로 작성해야 하며 엄격한 정적 분석을 수행하기 위해 컴파일러와 동적으로 연결되어야 한다.

소프트웨어 모델 검사

소프트웨어 모델 검사는 프로그램의 실행 속성을 증명하기 위한 알고리즘 분석이다.[4]이것은 주어진 정확한 사양에 대한 프로그램 동작에 대한 추론을 자동화한다.모델 점검과 심볼 실행은 기기 드라이버의 안전 중요 특성을 검증하는 데 사용된다.모델 체커에 대한 입력은 프로그램과 시간 안전 특성이다.출력은 프로그램이 올바르다는 증거나 특정 실행 경로 형태의 counterrexample에 의한 규격 위반이 존재한다는 것을 증명하는 것이다.

마이크로소프트의 정적 드라이버 검증 도구인 SDV(Static Driver Verifier)[5]는 윈도우 장치 드라이버에 대해 정적 분석을 사용한다.백엔드 분석 엔진 SLAM은 컴파일 시간 정적 확인을 위해 모델 점검과 심볼적 실행을 사용했다.각 API에 대해 드라이버가 준수해야 할 규칙은 C like Language SLIC(인터페이스 체크를 위한 Specification Language)에 명시되어 있다.분석 엔진은 API 사용 규칙 위반으로 이어질 수 있는 모든 경로를 찾아 드라이버 소스 코드를 통해 소스 레벨 오류 경로로 제시한다.내부적으로는 C 코드를 부울 프로그램과 이 프로그램에서 준수해야 할 규칙인 술어 집합으로 추상화한다.그런 다음 기호 모델 검사를 사용하여[6] 부울 프로그램에서 술어를 검증한다.

리눅스 커널 코드의 메모리 안전성과 부정확한 잠금 오류를 찾기 위해 모델 체커 VLAST(Berkeley Laze Option Software Verification Tool)[7]를 사용한다.드라이버 C 코드로 모델을 구축하기 위해 게으른 추상화라는[8] 추상화 알고리즘을 사용한다.최대 50K라인 코드로 C 프로그램의 시간적 안전성 특성 검증에 성공했다.또한 소스 코드의 변경이 이전 버전의 속성 증명에 영향을 미치는지 여부를 판단하기 위해 사용되며 Windows 장치 드라이버에서 시연된다.

Avinux는[9] 리눅스 장치 드라이브의 자동 분석을 용이하게 하는 또 다른 도구로 경계 모델 체커 CBMC 위에 구축되어 있다.[10]이 모델 체크 툴은 긴 카운터 예시 추적을 반환하고 정확한 불량 위치를 찾기 어렵기 때문에 버그 위치를 찾기 위한 결함 국산화 방법이 존재한다.[11]

실행 시간 분석

동적 프로그램 분석은 흥미로운 행동을 만들기에 충분한 시험 입력으로 프로그램을 실행함으로써 수행된다.Safe Drive는[12] 장치 드라이버의 유형 안전 위반을 감지하고 복구하기 위한 낮은 오버헤드 시스템이다.리눅스 네트워크 드라이버의 소스 코드를 4%만 변경하면 SafeDrive를 구현하고 리눅스 커널에 더 나은 보호 및 복구를 제공할 수 있었다.주 커널에서 장치 드라이버를 분리하기 위해 하드웨어를 사용하는 유사한 프로젝트가 바로 누크다.[13]이들은 장치 드라이버를 "nooks"라는 별도의 하드웨어 보호 도메인에 배치하고 각 페이지에 대한 별도의 권한 설정을 통해 드라이버가 도메인에 없지만 동일한 주소 공간을 공유하기 때문에 모든 커널 데이터를 읽을 수 있는 페이지를 수정하지 않도록 한다.

운전자의 결함으로 인한 운영체제의 자동 복구에 관한 이 분야의 또 다른 유사한 작업이 있다.MINIX 3는[14] 주요 결함을 격리하고 결함이 감지되며 고장 난 부품을 즉시 교체할 수 있는 운영체제다.

장치 드라이버 합성

결함의 검증과 격리의 대안은 장치 드라이버 개발 프로세스에 기술을 배치하여 결함을 더욱 견고하게 만드는 것이다.장치 사양과 운영 체제 기능을 고려하여 한 가지 방법은 해당 장치의 장치 드라이버를 합성하는 것이다.이것은 시스템 소프트웨어 개발에 드는 비용과 시간뿐만 아니라 인간이 도입한 오류를 줄이는 데 도움이 된다.모든 합성 방법은 하드웨어 장치 제조업체와 운영 체제 기능의 어떤 형태의 사양에 의존한다.

인터페이스 사양 언어

하드웨어 운용 코드는 대개 수준이 낮고 오류가 발생하기 쉽다.코드 개발 엔지니어는 일반적으로 부정확하거나 부정확한 정보를 포함하는 하드웨어 문서에 의존한다.하드웨어 기능을 표현하기 위한 몇 가지 인터페이스 정의 언어(IDL)가 있다.현대의 OS는 이러한 IDL을 사용하여 구성요소를 접착하거나 원격 절차 통화 IDL과 같이 이질성을 숨긴다.하드웨어 기능에도 동일하게 적용된다.이 섹션에서는 낮은 수준의 코딩을 추상화하고 코드를 생성하기 위해 특정 컴파일러를 사용하는 데 도움이 되는 도메인별 언어로 장치 드라이버를 작성하는 방법에 대해 논의한다.

Devil은[15] 기기와의 통신에 대한 높은 수준의 정의를 허용한다.하드웨어 구성요소는 I/O 포트와 메모리 맵 레지스터로 표현된다.그런 다음 이러한 사양은 드라이버 코드에서 호출할 수 있는 C 매크로 세트로 변환되어 낮은 레벨 함수를 쓰면서 프로그래머가 유발하는 오류를 제거한다.NDL은[16] Devil의 기능 향상으로 운전자를 운영 인터페이스로 설명한다.그것은 Devil의 인터페이스 정의 구문을 사용하며 레지스터 정의 집합, 레지스터에 접근하기 위한 프로토콜 및 장치 기능의 집합을 포함한다.그런 다음 장치 기능은 해당 인터페이스에서 일련의 작동으로 변환된다.장치 드라이버 생성을 위해서는 먼저 이러한 인터페이스 사양 언어로 드라이버 기능을 작성한 다음 로우 레벨 드라이버 코드를 생성하는 컴파일러를 사용해야 한다.

HAEL(Hardware Access Interface Language)[17]은 또 다른 도메인별 장치 드라이버 사양 언어다.드라이버 개발자는 다음과 같이 써야 한다.

  1. 장치 데이터 시트의 다양한 장치 레지스터 및 비트 필드를 설명하는 맵 설명을 등록하십시오.
  2. 버스 액세스를 위한 주소 공간 설명.
  3. 특정 시스템에서 장치의 인스턴스화.
  4. 장치에 액세스하는 데 제약이 있는 불변 규격.

HALE 컴파일러는 이러한 입력을 취하여 사양을 C 코드로 변환한다.

하드웨어 소프트웨어 공동 설계

하드웨어 소프트웨어 공동 설계에서 설계자는 그들끼리 통신하는 유한 상태 기계를 사용하는 시스템의 구조와 행동을 명시한다.그런 다음 하드웨어에 들어가는 구성 요소와 소프트웨어에 들어가는 구성 요소를 결정하기 전에 이러한 상태 기계에 대해 일련의 테스트, 시뮬레이션 및 공식 검증을 수행한다.하드웨어는 일반적으로 현장 프로그래머블 게이트 어레이(FPGA) 또는 애플리케이션별 집적회로(ASIC)로 수행되는 반면 소프트웨어 부분은 낮은 수준의 프로그래밍 언어로 번역된다.이 접근방식은 대부분 센서를 통해 환경과 지속적으로 상호작용하는 프로그램 가능한 부품의 집합으로 정의되는 임베디드 시스템에 적용된다.기존 기법은[18] 단순한 마이크로컨트롤러와 그 구동장치를 생성하기 위한 것이다.

독립 실행형 드라이버 합성

독립형 합성에서는 장치와 시스템 소프트웨어 모두 별도로 수행된다.이 장치는 HDL(Hardware Description Language)을 사용하여 모델링되며 소프트웨어 개발자는 HDL 사양에 액세스할 수 없다.하드웨어 개발자는 장치의 데이터 시트에 장치 인터페이스를 표시했다.드라이버 개발자는 데이터 시트에서 장치의 레지스터 및 메모리 레이아웃과 유한 상태 기계 형태의 행동 모델을 추출한다.이것은 인터페이스 언어 섹션에서 설명하는 도메인별 언어로 표현된다.마지막 단계에는 이러한 규격에서 코드를 생성하는 작업이 포함된다.

Termite[19] 툴은 드라이버를 생성하기 위해 세 가지 사양을 사용한다.

  1. 장치 사양 : 장치 데이터 시트에서 얻은 장치 레지스터, 메모리 및 인터럽트 서비스 사양
  2. 기기 등급 규격 : 관련 기기 I/O 프로토콜 표준에서 얻을 수 있다.예를 들어 이더넷의 경우 이더넷 LAN 표준은 이러한 컨트롤러 장치의 일반적인 동작을 설명한다.이것은 보통 패킷 전송, 자동 협상 완료, 링크 상태 변경 등과 같은 일련의 이벤트로 암호화된다.
  3. OS 사양 : 드라이버와의 OS 인터페이스를 기술한다.보다 구체적으로, 요청 OS가 드라이버에게 할 수 있는 것, 이러한 요청의 순서, 그리고 OS가 이러한 요청에 대한 대가로 드라이버가 기대하는 것.각 전환이 OS에 의한 드라이버 호출, 드라이버에 의한 콜백 또는 프로토콜 지정 이벤트에 해당하는 상태 머신을 정의한다.

이러한 규격에 따라 Termite는 OS 요청의 유효한 순서를 일련의 장치 명령으로 변환하는 드라이버 구현을 생성할 것이다.인터페이스의 공식적인 사양으로 인해 Termite는 안전성과 강도 속성을 가진 드라이버 코드를 생성할 수 있다.

RevNIC는 기존 드라이버를 역엔지니어링하여 새로운 플랫폼을 위한 이동 가능하고 안전한 드라이버를 만드는 매우 흥미로운 해킹 노력을 해왔다.[20]드라이버를 역설계하기 위해 상징적이고 구체적인 실행으로 드라이버를 실행함으로써 하드웨어 I/O 작업을 도청한다.도청기의 출력은 신디사이저에 공급되며, 신디사이저는 해당 장치 등급의 보일러플레이트 템플릿과 함께 이러한 다중 추적에서 원래 드라이버의 제어 흐름 그래프를 재구성한다.연구자들은 이러한 방법을 사용하여 네트워크 인터페이스용 일부 Windows 드라이버를 다른 Linux 및 임베디드 운영 체제에 포팅했다.

비판

많은 정적 분석 도구가 널리 사용되는 반면, 많은 운전자 종합 및 검증 도구는 실제로 광범위하게 수용되지 않았다.그 이유 중 하나는 드라이버가 여러 장치를 지원하는 경향이 있고 드라이버 합성 작업은 일반적으로 지원되는 장치당 하나의 드라이버를 생성하여 잠재적으로 많은 수의 드라이버를 발생시킬 수 있기 때문이다.또 다른 이유는 운전자도 일부 처리를 하고 운전자의 상태 기계 모델은 처리를 묘사할 수 없기 때문이다.[21]

결론

이 글에서 조사한 다양한 검증과 합성 기법에는 나름대로 장단점이 있다.예를 들어, 런타임 장애 분리에는 성능 오버헤드가 있는 반면 정적 분석에는 모든 유형의 오류가 포함되지 않는다.디바이스 드라이버 합성의 완전한 자동화는 아직 초기 단계에 있으며 향후 연구 방향이 유망하다.오늘날 인터페이스 사양에 사용할 수 있는 많은 언어가 결국 하나의 형식으로 통합될 수 있다면 진전은 촉진될 것이다. 단, 장치 공급업체와 운영 체제 팀이 이를 보편적으로 지원한다.그러한 표준화 노력의 보상은 미래에 신뢰할 수 있는 장치 드라이버의 완전 자동화된 합성의 실현일 수 있다.

참조

  1. ^ 아르카나 가나파티, 비지 가나파티, 데이비드 패터슨."Windows XP 커널 충돌 분석".2006년 대규모 설치 시스템 관리 회의의 절차서, 2006.
  2. ^ A. 추, J. 양, B.Chelf, S. Hallem and D.엥글러.운영체제 오류에 대한 실증적 연구2001년 SOSP에서
  3. ^ 엥글러, 도슨과 첼프, 벤자민과 츄, 앤디와 할렘, 세스."시스템별 프로그래머 작성 컴파일러 확장을 사용하여 시스템 규칙 확인"2000년 제4차 운영체제 설계 및 구현 심포지엄 개최안
  4. ^ 얄라와 란짓과 마금다르와 루팍과"소프트웨어 모델 확인".ACM 계산 조사.2009
  5. ^ 토마스 볼, 엘라 바니모바, 바이런 쿡, 블라디미르 레빈, 야콥 리히텐베르크, 콘 맥가비, 보후스 온드루섹, 스리람 라자마니.그리고 압둘라 유스튜너 입니다."장치 드라이버의 엄격한 정적 분석", In SIGOPS Operator.2006년 제40권 제2장.
  6. ^ 맥밀런, 케네스 L. "심볼릭 모델 확인"클루워 학술 출판사, 1993.
  7. ^ 토마스 A.헨징거, 란지트 얄라, 루팍 마금다르, 그레고아르 수트레."BLAST를 사용한 소프트웨어 검증".2003년 SPIN에서.
  8. ^ 토마스 A.헨징거, 란지트 얄라, 루팍 마금다르, 그레고아르 수트레.2002년 ACM SIGLAN-SIGACT 프로그래밍 언어 원리에 관한 회의의 "레이지 추상화"
  9. ^ H. Post, W. Küchlin."Linux Device 드라이버 검증을 위한 정적 분석 통합"The 6th Internal.통합 형식 방법, 2007.
  10. ^ 에드먼드 클라크, 다니엘 크로닝, 플라비오 레르다."A Tool for Check ANSI-C Programs".TACAS, 2004년
  11. ^ 토마스 볼, 마유르 나이크, 그리고 시람 K.라자마니죠"증상에서 원인에 이르기까지: counterexample trace의 오류 위치 지정"ACM SIGLAN 공지사항, 2003.
  12. ^ 펑주, 제레미 콘딧, 재커리 앤더슨, 일리야 백락, 롭 에널스, 매튜 하렌, 조지 네쿨라, 에릭 브루어."SafeDrive: 언어 기반 기술을 사용한 안전하고 복구 가능한 확장".2006년 7차 OSDI.
  13. ^ 마이클 M.스위프트, 스티븐 마틴, 헨리 M레비, 그리고 수잔 J. 에거스."Nooks: 신뢰할 수 있는 장치 드라이버를 위한 아키텍처 ".2002년 ACM SIGOPS 10번지.
  14. ^ 조릿 N.Herder, Herbert Bos, Ben Gras, Philip Homburg, Andrew S.타넨바움."MINIX 3: 신뢰성이 높은 자체 수리 운영 체제"SIGOPS Operator에서.2006년 시스템 40차 개정판
  15. ^ 파브리스 메릴론, 로랑 리비유레, 찰스 콘젤, 레나우드 말렛, 길레스 뮬러."악마: 하드웨어 프로그래밍용 IDL"제4차 운영체제 설계 및 구현 심포지엄 회의의 절차서, 2000. 4.
  16. ^ Christopher L. Conway와 Stephen A.에드워즈"NDL: 장치 드라이버를 위한 도메인별 언어".ACM SIGPlan 통지서 39, 2004.
  17. ^ J. Sun, W. Yuan, M. Kallahalla, N.이슬람. "HACE: 쉽고 정확한 장치 액세스를 위한 언어"2005년 임베디드 소프트웨어에 관한 ACM 회의의 Proc.
  18. ^ 펠리스 발라린 외"하드웨어-소프트웨어의 Embedded Systems 공동 설계. 폴리스 접근법." 클루워어 학술 출판사, 1997.
  19. ^ 레오니드 리지크, 피터 처브, 이호르 쿠즈, 에티엔 르 수우르, 제르노 하이저."Termite를 사용한 자동 장치 드라이버 합성".2009년 제22회 ACM 운영체제 원칙 심포지엄 진행 중.
  20. ^ 비탈리 치푸노프와 조지 칸데아."RevNIC를 사용하는 바이너리 장치 드라이버의 역 엔지니어링". 제5회 ACM SIGOPS/EuroSys, 2010.
  21. ^ 아심 카다브와 마이클 M.제17회 ACM 회의의 신속한 "현대적 장치 드라이버의 이해" 언어 프로그래밍 및 운영체제 구축 지원 회의

외부 링크