프라마-C

Frama-C
프라마소프트와 혼동하지 말자.
프라마-C
Frama-C logo, full.png
개발자코미사리아 아 레네르기 아토미크(CEA-List)와 인리아
리포지토리
기록 위치OCAML
운영 체제Microsoft Windows, FreeBSD, OpenBSD, Linux, Mac OS X
다음에서 사용 가능영어
유형형식 확인, 정적 코드 분석
면허증대부분 LGPL, BSD 라이센스 하에 일부 부품
웹사이트frama-c.com

Frama-C는[1] C 프로그램의 모듈 분석을 위한 프레임워크를 의미한다.Frama-C는 C 프로그램용 상호운용 가능한 프로그램 분석기 세트다.Frama-C는 프랑스의 Commissarity á L'énergie Atomique et aux Energies Alternatives (CEA-List)[2]와 Inria에 의해 개발되었다.그것은 또한 핵심인프라 이니셔티브로부터 자금을 받았다.Frama-C는 정적 분석기로서 프로그램을 실행하지 않고 검사한다.그 이름에도 불구하고, 이 소프트웨어는 프랑스 프로젝트인 Framasoft와는 관련이 없다.

건축

Frama-C는 Eclipse(소프트웨어)나 KIMP와 견줄 만한 모듈형 플러그인 아키텍처를[3] 가지고 있다.

Frama-C는 추상 구문 트리를 생성하기 위해 CIL(C 중간 언어)에 의존한다.추상 구문 트리는 ANSI/ISO C 사양 언어(ACSL)로 작성된 주석을 지원한다.

여러 모듈이 추상 구문 트리를 조작하여 ANSI/ISO C 사양 언어(ACSL) 주석을 추가할 수 있다.자주 사용되는[vague] 플러그인은 다음과 같다.

  • 값 분석 – 프로그램의 각 변수에 대한 값 또는 가능한 값 집합을 계산한다.이 플러그인은 추상적 해석 기법을 사용하며 많은 다른 플러그인은 그 결과를 이용한다.
  • 제시 – 연역적인 방식으로 속성을 검증한다.제시는 증명 의무가 Z3, Simply, Alt-Ego와 같은 자동 정리 프로바이더나 Coq 또는 Why와 같은 인터랙티브 정리 프로바이더에게 보내질 수 있도록 하기 위해 Why[4] or Why3 백엔드에 의존한다.제시를 이용하면, 버블 소트나 장난감 전자 투표 시스템의 구현이 각각의 사양을 만족시키는 것으로 증명될 수 있다.분리논리에서 영감을 받은 분리기억 모델을 사용한다.
  • WP(Weakest President) – 제시와 유사하게 연역적인 방식으로 속성을 검증한다.제시와 달리 메모리 모델과 관련한 파라미터화에 중점을 두고 있다.WP는 C 프로그램을 Why 언어로 직접 컴파일하는 제시와 달리 가치분석 플러그인 등 다른 Frama-C 플러그인과 협력하도록 설계됐다.WP는 Why3 플랫폼을 선택적으로 사용하여 많은 자동화되고 상호작용적인 프로바이더를 호출할 수 있다.
  • 영향 분석 – C 소스 코드 수정의 영향을 강조한다.
  • 슬라이싱 – 프로그램을 슬라이싱할 수 있음그것은 주어진 특성들을 보존하는 더 작은 새로운 C 프로그램의 생성을 가능하게 한다.[5]
  • 예비 코드 – C 프로그램에서 쓸모 없는 코드를 제거하십시오.

기타 플러그인은 다음과 같다.

  • 도미네이터 – 진술의 도미네이터와 사후 도미네이터를 계산한다.
  • 분석으로부터 – 기능 의존성을 계산한다.

특징들

Frama-C는 다음과 같은 목적으로 사용할 수 있다.

  • 당신이 쓰지 않은 C코드를 이해하기 위해서입니다.특히 Frama-C는 일련의 값을 관찰하고, 프로그램을 더 짧은 프로그램으로 자르고, 프로그램을 탐색할 수 있게 해준다.
  • 코드에 형식적인 속성을 증명하기 위해ANSI/ISO C 사양 언어로 작성된 사양을 사용하면 가능한 모든 동작에 대해 코드의 속성을 보장할 수 있다.Frama-C는 부동 소수점 번호를 처리한다.[6]
  • 사용자 지정 플러그인을 통해 C 소스 코드에 코딩 표준 또는 코드 규칙을 적용하려면 다음과 같이 하십시오.[7]
  • 일부 보안 결함에[8] 대해 C 코드를 계측하려면 다음과 같이 하십시오.

참고 항목

참조

  1. ^ "Frama-C". frama-c.com. Retrieved 2016-11-05.
  2. ^ CEA LIST. "CEA LIST, Smart digital systems". Retrieved 2016-11-05.
  3. ^ Pascal Cuoq; et al. (August 2009). "Experience report: OCaml for an industrial-strength static analysis framework". Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming. 44 (9): 281–286. doi:10.1145/1631687.1596591.
  4. ^ "Why homepage".
  5. ^ Benjamin Monate; Julien Signoles (2008). "Slicing for Security of Code". Trusted Computing - Challenges and Applications. Lecture Notes in Computer Science. Vol. 4968/2008. doi:10.1007/978-3-540-68979-9_10. ISBN 978-3-540-68978-2.
  6. ^ Sylvie Boldo; Thi Minh Tuyen Nguyen (2010). "Hardware-independent proofs of numerical programs" (PDF). Proceedings of NFM 2010.
  7. ^ David Delmas; Stéphane Duprat; Victoria Moya Lamiel; Julien Signoles. "Taster, a Frama-C plug-in to enforce Coding Standards" (PDF). Embedded Real Time Software and Systems 2010, Toulouse, France.
  8. ^ Jonathan-Christofer Demay; Éric Totel; Frédéric Tronel (2009). "Automatic Software Instrumentation for the Detection of Non-control-data Attacks". Recent Advances in Intrusion Detection. Lecture Notes in Computer Science. Vol. 5758/2009. pp. 348–349. doi:10.1007/978-3-642-04342-0_19. ISBN 978-3-642-04341-3.

외부 링크