정적 프로그램 분석

Static program analysis
시리즈의 일부
소프트웨어 개발
핵심 활동
패러다임 및 모델
방법론 및 프레임워크
지원 분야
프랙티스
도구들
지식의 표준과 본문
용어집
개요

컴퓨터 과학에서 정적 프로그램 분석(static program analysis)은 프로그램을 [1][2]실행하는 동안 실행되는 동적 프로그램 분석과는 대조적으로 실행하지 않고 수행되는 컴퓨터 프로그램의 분석입니다.

이 용어는 일반적으로 자동화된 도구에 의해 수행되는 분석에 적용되며, 인체 분석은 일반적으로 "프로그램 이해", 프로그램 이해 또는 코드 검토라고 불립니다.이들 중 마지막에는 소프트웨어 검사 및 소프트웨어 실사도 사용됩니다.대부분의 경우 분석은 프로그램 소스 코드의 일부 버전에 대해 수행되며, 다른 경우에는 객체 코드의 어떤 형태에 대해 수행됩니다.

근거

도구에 의해 수행되는 분석의 정교함은 개별 진술 및 [3]선언의 동작만을 고려하는 분석에서 프로그램의 완전한 소스 코드를 분석에 포함하는 분석까지 다양합니다.분석을 통해 얻은 정보의 용도는 가능한 코딩 오류(예: 보풀 도구)를 강조하는 것에서부터 주어진 프로그램에 대한 특성을 수학적으로 증명하는 공식 방법(예: 사양과 일치하는 동작)에 이르기까지 다양합니다.

소프트웨어 메트릭과 리버스 엔지니어링은 정적 분석의 한 형태로 설명할 수 있습니다.소프트웨어 메트릭의 도출과 정적 분석은, 특히 임베디드 시스템의 작성에 있어서, 이른바 소프트웨어 품질 [4]목표를 정의함으로써, 한층 더 함께 전개되고 있습니다.

정적 분석의 상업적 용도는 안전에 중요한 컴퓨터 시스템에서 사용되는 소프트웨어의 속성을 검증하고 잠재적으로 취약한 [5]코드를 찾는 데 있어 증가하고 있습니다.예를 들어, 다음 업계에서는 정적 코드 분석의 사용을 점점 더 정교해지고 복잡한 소프트웨어의 품질을 개선하기 위한 수단으로 인식하고 있습니다.

  1. 의료 소프트웨어:미국 식품의약국(FDA)은 의료기기에 [6]대한 정적 분석의 사용을 확인했다.
  2. 원자력 소프트웨어:영국에서 원자력규제국(ONR)은 원자로 보호시스템에 [7]대한 정적 분석 사용을 권고한다.
  3. 항공 소프트웨어(동적 [8]분석과 조합)
  4. 자동차 및 기계 (기능적 안전 기능은 각 자동차 제품 개발 단계에서 필수적인 부분을 형성합니다, ISO 26262, 8장).

VDC Research가 2012년에 실시한 조사에 따르면 조사 대상 임베디드 소프트웨어 엔지니어의 28.7%가 현재 정적 분석 툴을 사용하고 있으며 39.7%는 [9]2년 이내에 이러한 툴을 사용할 것으로 예상하고 있습니다.2010년의 조사에 의하면, 유럽 연구 프로젝트의 인터뷰에 응한 개발자의 60%가, 적어도 기본적인 IDE 내장 정적 분석기를 사용하고 있는 것을 알 수 있었습니다.단, 약 10%만이 기타(아마도 더 고급)[10] 분석 도구를 추가로 사용하였습니다.

애플리케이션 시큐러티 업계에서는, 스태틱 애플리케이션 시큐러티 테스트(SAST)라는 이름도 사용합니다.SAT는 Microsoft가[11] 정의한SDL 등 보안 개발 라이프 사이클(SDL)의 중요한 부분이며 소프트웨어 [12]회사에서는 일반적인 작업입니다.

도구 종류

OMG(Object Management Group)는 소프트웨어 품질 측정 및 평가에 필요한 소프트웨어 분석 유형에 대한 연구를 발표했습니다.이 문서에서는 "CISQ 권장 사항에 따라 탄력적이고 안전하고 효율적이며 쉽게 변경되는 IT 시스템을 제공하는 방법"에 대해 세 가지 수준의 소프트웨어 [13]분석을 설명합니다.

유닛 레벨
특정 프로그램 또는 서브루틴 내에서 해당 프로그램의 컨텍스트에 연결하지 않고 수행되는 분석입니다.
테크놀로지 레벨
문제를 찾아 명백한 잘못된 긍정을 피하기 위해 프로그램 전체의 전체적인 의미적 뷰를 얻기 위해 단위 프로그램 간의 상호작용을 고려하는 분석입니다.예를 들어 Android 기술 스택을 정적으로 분석하여 권한 오류를 [14]찾을 수 있습니다.
시스템 레벨
하나의 특정 기술 또는 프로그래밍 언어에 국한되지 않고 단위 프로그램 간의 상호작용을 고려하는 분석입니다.

한층 더 레벨의 소프트웨어 분석을 정의할 수 있습니다.

미션/비즈니스 레벨
기업 또는 프로그램/미션 계층 활동의 일부로서 소프트웨어 시스템 내에서 실행되는 비즈니스/미션 계층 용어, 규칙 및 프로세스를 고려한 분석.이러한 요소는 하나의 특정 기술 또는 프로그래밍 언어에 국한되지 않고 구현되며, 많은 경우 여러 언어로 분산되지만 미션 보증을 위한 시스템 이해를 위해 정적으로 추출 및 분석됩니다.

형식적인 방법

주요 기사:형식적인 방법

형식적 방법은 소프트웨어(및 컴퓨터 하드웨어)의 분석에 적용되는 용어이며, 그 결과는 순전히 엄격한 수학적 방법을 사용하여 얻어진다.사용된 수학적 기법에는 표현적 의미론, 공리적 의미론, 운영적 의미론, 추상적 해석이 포함된다.

정지 문제에 대한 간단한 감소에 의해 (튜링 완료 언어에 대해) 임의의 프로그램에서 가능한 모든 런타임 오류(또는 더 일반적으로 프로그램의 최종 결과에 대한 사양 위반의 종류)를 찾는 것은 결정할 수 없다는 것을 증명할 수 있다: 항상 진실이라고 대답할 수 있는 기계적인 방법은 없다.ulli는 임의의 프로그램에서 런타임 오류가 발생할 수 있는지 여부를 나타냅니다.이 결과는 1930년대의 처치, 괴델, 튜링의 작품에서 유래한다.많은 결정 불가능한 질문들과 마찬가지로, 사람들은 여전히 유용한 대략적인 해답을 제시하려고 시도할 수 있다.

정식 정적 분석의 구현 기법에는 다음과 같은 것이 있습니다.[15]

  • 추상 해석 - 모든 문장이 추상 기계 상태에 미치는 영향을 모델링합니다(즉, 각 문장과 선언의 수학적 특성에 따라 소프트웨어를 '실행'합니다).이 추상 기계는 시스템의 동작을 지나치게 근사하게 표현합니다. 따라서 추상 시스템은 불완전성을 희생하면서 분석하기가 더 쉬워집니다(원래 시스템에 맞는 모든 속성이 추상 시스템에 적용되는 것은 아닙니다).그러나 적절하게 수행된다면 추상적 해석은 타당하다(추상 시스템에 참된 모든 속성은 원래 시스템의 [16]참된 속성에 매핑될 수 있다).
  • 가능한 값 집합에 대한 정보를 수집하기 위한 격자 기반 기술인 데이터 흐름 분석
  • Hoare logic은 컴퓨터 프로그램의 정확성에 대해 엄격하게 추론하기 위한 일련의 논리 규칙을 가진 형식적인 시스템입니다.일부 프로그래밍 언어(SPARK 프로그래밍 언어(Ada의 서브셋) 및 Java 모델링 언어)에 대한 도구가 지원됩니다.JML: ESC/Java 및 ESC/Java2, ACSL(ANSI/ISO C Specification Language)로 확장되는 C 언어용 Frama-C WP(최저 사전 조건) 플러그인을 사용합니다.
  • 모델 확인, 추상화에 의해 유한 상태를 가지거나 유한 상태로 축소될 수 있는 시스템을 고려합니다.
  • 코드 내의 특정 포인트에서 변환된 변수의 값을 나타내는 수학식을 도출하는 데 사용되는 기호 실행입니다.

데이터 중심 정적 분석

데이터 중심 정적 분석에서는 코딩 [17][better source needed]규칙을 추론하기 위해 많은 양의 코드를 사용합니다.예를 들어 GitHub의 모든 Java 오픈 소스 패키지를 사용하여 좋은 분석 전략을 배울 수 있습니다.규칙 추론은 기계 학습 [18]기술을 사용할 수 있습니다.예를 들어 객체 지향 API를 사용하는 방식이 너무 많이 어긋나면 [19]버그일 가능성이 높은 것으로 나타났다.과거의 많은 수정이나 [17][better source needed]경고로부터 학습할 수도 있습니다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ Wichmann, B. A.; Canning, A. A.; Clutterbuck, D. L.; Winsbarrow, L. A.; Ward, N. J.; Marsh, D. W. R. (Mar 1995). "Industrial Perspective on Static Analysis" (PDF). Software Engineering Journal. 10 (2): 69–75. doi:10.1049/sej.1995.0010. Archived from the original (PDF) on 2011-09-27.
  2. ^ Egele, Manuel; Scholte, Theodoor; Kirda, Engin; Kruegel, Christopher (2008-03-05). "A survey on automated dynamic malware-analysis techniques and tools". ACM Computing Surveys. 44 (2): 6:1–6:42. doi:10.1145/2089125.2089126. ISSN 0360-0300. S2CID 1863333.
  3. ^ Khatiwada, Saket; Tushev, Miroslav; Mahmoud, Anas (2018-01-01). "Just enough semantics: An information theoretic approach for IR-based software bug localization". Information and Software Technology. 93: 45–57. doi:10.1016/j.infsof.2017.08.012.
  4. ^ "소스 코드의 소프트웨어 품질 목표" 2015-06-04년 Wayback Machine(PDF)에 보관.진행: 임베디드 실시간 소프트웨어 및 시스템 2010 컨퍼런스, ERTS2010.org, 툴루즈, 프랑스: Patrick Briand, Martin Brochet, Tierry Cambois, Emanuel Coutenceau, Olivier Guetta, Daniel Mainberte, Frederic Mondot, Patrick Munier, Frégio, Frape
  5. ^ 정밀 정적 및 런타임 분석을 통한 소프트웨어 보안 향상 2011-06-05년 Wayback Machine(PDF), Benjamin Livshits 섹션 7.3 "보안용 정적 기법"에서 아카이브되었습니다.스탠포드 박사학위 논문, 2006.
  6. ^ FDA (2010-09-08). "Infusion Pump Software Safety Research at FDA". Food and Drug Administration. Archived from the original on 2010-09-01. Retrieved 2010-09-09.
  7. ^ 컴퓨터 기반 안전 시스템 - 디지털 컴퓨터 기반 보호 시스템의 소프트웨어 측면을 평가하기 위한 기술 지침
  8. ^ 용지 CAST-9를 배치합니다. Wayback Machine // FAA, 인증기관 소프트웨어 팀(CAST), 2002년 1월 "검증"에서 보관된 소프트웨어 보증에 대한 안전 엔지니어링 접근 평가 고려사항 2013-10-06.정적 분석과 동적 분석의 조합은 신청자/개발자가 지정하고 소프트웨어에 적용해야 한다."
  9. ^ VDC Research (2012-02-01). "Automated Defect Prevention for Embedded Software Quality". VDC Research. Archived from the original on 2012-04-11. Retrieved 2012-04-10.
  10. ^ 프라우스, 크리스찬 R., 르네 라이너스, 실비야 덴체바."고분산 연구 프로젝트에서 도구 지원에 대한 경험적 연구"글로벌 소프트웨어 엔지니어링(ICGSE), 2010년 제5회 IEEE 국제회의 개최.IEEE, 2010 http://ieeexplore.ieee.org/ielx5/5581168/5581493/05581551.pdf
  11. ^ 하워드 씨와 S 씨립너.시큐러티 개발 라이프 사이클:SDL:시큐어성이 뛰어난 소프트웨어를 개발하는 프로세스.Microsoft Press, 2006.ISBN 978-0735622142
  12. ^ 아킴디브루커와 우웨 소단.2014-10-21 웨이백 머신에서 아카이브된 대규모 정적 애플리케이션 보안 테스트 배포GI Sicherheit 2014에서.정보학 강의 노트, 228, 91-101페이지, GI, 2014.
  13. ^ "OMG Whitepaper CISQ - Consortium for Information & Software Quality" (PDF). Archived (PDF) from the original on 2013-12-28. Retrieved 2013-10-18.
  14. ^ Bartel, Alexandre; Klein, Jacques; Monperrus, Martin; Le Traon, Yves (1 June 2014). "Static Analysis for Extracting Permission Checks of a Large Scale Framework: The Challenges and Solutions for Analyzing Android". IEEE Transactions on Software Engineering. 40 (6): 617–632. arXiv:1408.3976. doi:10.1109/tse.2014.2322867. S2CID 6563188.
  15. ^ Vijay D’Silva; et al. (2008). "A Survey of Automated Techniques for Formal Software Verification" (PDF). Transactions On CAD. Archived (PDF) from the original on 2016-03-04. Retrieved 2015-05-11.
  16. ^ Jones, Paul (2010-02-09). "A Formal Methods-based verification approach to medical device software analysis". Embedded Systems Design. Archived from the original on July 10, 2011. Retrieved 2010-09-09.
  17. ^ a b "Learning from other's mistakes: Data-driven code analysis". www.slideshare.net. 13 April 2015.
  18. ^ Oh, Hakjoo; Yang, Hongseok; Yi, Kwangkeun (2015). "Learning a strategy for adapting a program analysis via bayesian optimisation". Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2015. pp. 572–588. doi:10.1145/2814270.2814309. ISBN 9781450336895. S2CID 13940725.
  19. ^ Monperrus, Martin; Mezini, Mira (2013). "Detecting missing method calls as violations of the majority rule". ACM Transactions on Software Engineering and Methodology. 22 (1): 1–25. arXiv:1306.0762. doi:10.1145/2430536.2430541. S2CID 1212778.

추가 정보