iOS Infer 정적 코드 분석

5698 단어

잡담

  • Monoidics는 2009년에 창립되었고 소프트웨어의 안정성과 안전성을 분석하고 검토하는 것이 특기입니다.이 회사의 Infer Static Analyzer 제품은 메모리 오버플로우, 불법 포인터 참조 등의 오류를 방지하기 위해 코드의 보안 취약성을 감지합니다.또한 Infer X-Ray라는 또 다른 제품은 엔지니어가 소프트웨어의 품질을 시각적으로 측정하고 개선해야 할 관건적인 지역 리스크를 식별하는 데 도움을 줄 수 있다.
  • 페이스북은 영국 휴대전화 코드 검증 소프트웨어 개발 업체인Monoidics를 인수했다.거래가 완료되면 일부 Monoidics 엔지니어들은 페이스북 런던 사무소에 가입해 업무를 볼 것이다.페이스북은 Monoidics가 개발한 휴대전화 코드 검증 및 버그 분석 기술
    • 을 적용할 예정이다.

    이론적 기초(절차 검증)

  • Hoare Logic(호르 논리): Hoare 논리(Floyd – Hoare 논리라고도 부른다)는 영국 컴퓨터 과학자 C. A. R. Hoare가 개발한 형식 시스템으로 그 다음에 Hoare와 다른 연구자들에게 정제되었다.그것은 Hoare 1969년의 논문인'컴퓨터 프로그램의 공리적 기초'에 발표되었다.이 시스템의 용도는 엄격한 수리 논리 추리 컴퓨터 프로그램의 정확성을 사용하기 위해 논리 규칙을 제공하는 것이다.Hoare 논리의 중심 특징은 Hoare 삼원조이다.이런 삼원조는 코드의 집행이 어떻게 계산의 상태를 바꾸는지 설명한다.
  • Separation Logic and Bi-abduction: 분리 논리는 홀 논리의 확장입니다.
  • 페이스북 인퍼는 논리로 프로그램의 실행을 추리하지만 이런 방식으로 수백만 줄의 코드량을 추리하는 응용은 매우 어렵다.이론적으로 볼 때 검사해야 할 코드의 수량은 예상한 수량보다 많을 것이다.이러한 규모와 속도는 더 높은 수학 모델이 필요하다. 페이스북 인퍼는 논리 분리와bi-abduction 두 가지 기술을 사용했다.
  • 논리적 분리는 페이스북 Infer 분석이 응용 저장소의 독립된 작은 부분을 추정할 수 있도록 하는 이론으로 한 걸음 한 걸음 저장소의 완전성을 고려하지 않는다.모든 단계의 저장 완전성을 고려하는 것은 현재의 대형 주소록 가상 메모리 프로세서에 있어서 매우 어려운 일이기 때문이다.
  • Bi-abduction은 논리적 추리 기법으로 페이스북 Infer가 응용 코드의 독립된 부분의 행위 특성을 발굴할 수 있다.실행할 때 이러한 특성을 저장한 후 페이스북은 소프트웨어에서 바뀐 부분만 분석하고, 다른 부분은 이전의 분석 결과를 그대로 적용할 수 있다.
  • 이 몇 가지 방법을 결합하면 우리의 분석기는 몇 분 안에 수백만 줄의 코드에서 수정된 코드에 존재하는 복잡한 문제를 찾을 수 있다.


    • 발췌하다

  • 역사: 코드 검사 이론에서 10억 명을 위한 서비스의 탈바꿈까지
  • 소프트웨어의 자동 검사는 컴퓨터 과학 지역사회에서 장기적으로 의존하는 목표이다.페이스북 인퍼는 이 분야에서 홀 논리와 추상적 해석을 포함하는 기본적인 실현을 구축했다.페이스북에 가입하기 전에 우리는 다른 인프라 시설의 개발에 참여했고'논리적 분리'는 소프트웨어 자동 검사를 실현할 수 있는 결과로 사람들의 시야에 나타났다.
  • 논리 분리는 컴퓨터 과학 분야의 중대한 돌파구이다. - 새로운 수학 논리는 컴퓨터 메모리의 변화를 묘사하는 데 사용된다.우리는 이 이론을 운용하고 자동화하는 데 전념하여 일련의 원형 도구(예를 들어 Smallfoot,Space Invader,Abductor)를 만들어 이러한 추리 논리를 지탱하는 데 전념하였고bi-abduction은 모듈화 분석 프로그램의 효과적인 형식이라는 것을 최종적으로 발견하였다.
  • 상술한 연구 성과를 바탕으로 우리는 2009년에Monoidics라는 회사를 창립했다.Monoidics는 2013년에 페이스북에 가입했습니다. 그 이후 저희는 지속적인 개발과 배치 스타일로 저희 제품을 개발했습니다. 저희 분석기팀과 페이스북 모바일 소프트웨어 개발 엔지니어들의 끊임없는 노력으로 저희 분석기는 크게 향상되었습니다.페이스북 코드 라이브러리에 활용될 때 코드 검사 기술이 빠르게 발전할 수 있음을 보여줬다.

  • 미래 전망
  • 프로그램 검사는 지역사회를 활발하게 연구하고 전망이 밝은 분야이다.페이스북에서 우리는 이번 여행을 1%밖에 완성하지 못했다고 말했다.프로그램 검사 분야에는 아직도 우리가 완성해야 할 일이 많다.그러나 우리의 끊임없는 노력에 따라 우리는 이 분야의 성과가 소프트웨어 엔지니어들에게 더 많은 가치를 해방시킬 것이라고 믿는다.우리는 미래를 전망할 수 있다. 당신의 도움으로 프로그램 검사 기술은 더 많은, 더 유용한 기술을 제공하여 우리의 코드를 더욱 믿음직스럽고 효율적으로 할 수 있다.


    • About Infer

  • 인퍼는 페이스북이 OCAml로 개발한 자바, C, Objective-C 코드를 정적 검사, 분석하는 도구이다.모바일 애플리케이션을 발표하기 전에 코드를 분석하여 잠재적인 문제점을 찾아내는 데 쓰인다.페이스북은 안드로이드, iOS, 페이스북 메신저, 인스타그램 등 페이스북의 앱을 분석하기 위해 이 도구를 사용한다.현재, 이것은 주로 다음과 같은 오류 유형을 검사한다. 빈 바늘의 간접 인용, 자원, 메모리 유출, 이 몇 가지 버그는 이동 개발에서 매우 가볍고 치명적이다.
  • 누구나 Infer 검사 애플리케이션을 사용할 수 있다. 이는 심각한 버그를 발표하기 전에 억제하고 애플리케이션 붕괴와 성능 저하를 방지할 수 있다.
  • 작업 흐름에서의 응용
  • 정적 분석 도구는 일반적으로 개발 단계에서 사용된다.이러한 도구의 본질은 개발 프로세스 또는 CI/CD 워크플로우의 한 단계로서 테스트 도구입니다.그것들은 디버거를 대체할 수 없다. 왜냐하면 그들은 작업할 때 코드가 이미 컴파일되었기 때문이다.그것들도 생산 환경에서의 오류 추적기를 대체할 수 없다. 코드가 생산 환경에 노출된 후에 동적 입력이 적중될 때만 발생하기 때문이다.그러나 이 두 환경 사이에 공간이 존재하는데 이곳에서 인퍼와 같은 도구는 매우 유용하다.예를 들어, 당신은 Infer를 개발 환경과 생산 환경의 중간 단계로 삼을 수 있습니다.Infer는 이러한 상황에서 온라인에 접속하기 전에 뚜렷한 버그를 미리 발견하는 데 도움을 줄 수 있다.이것은 사용자에게 최소한 Takipi 패널의 문제를 줄일 수 있습니다. 만약 Jenkins를 지속적인 개발 모델로 사용한다면, 버전마다 Infer를 실행하고, 던진 빨간색 표시를 볼 수 있습니다.


    • Limitations,etc

  • 당신이 run Infer on your 프로젝트에서 아주 좋은 결과를 얻을 수도 있지만 그렇지 않을 수도 있다는 것을 분명히 알아야 한다.
  • 페이스북은 자신의 코드 창고의 코드에 따라 인퍼의 문제점을 잘 복구했지만 인퍼를 다른 임의의 코드 라이브러리에 적용할 때 큰 오류 경고에 부딪힐 수 있다.
  • Infer를 자신의 코드에 적용할 때 우리가 얻은 결과가 결함이 있더라도 참고 가치가 있을 수 있기 때문에 우리는 이러한 분석 결과에 따라 우리의 코드를 개선할 수 있다.적어도 나는 우리 프로젝트의 코드를 테스트할 때 발견하기 어려운 여러 개의 버그를 발견했다. 예를 들어strong식delegate,dd는nil의object를 수조에 넣고 잠재적인 메모리 유출을 일으킬 수 있다.
  • 현재 Infer는 리포트와 같은 일부 버그 types를 할 수 있다. 전형적인 것은 다음과 같다.
  • null pointers
  • memory or resource leaks
  • 기술이나 오보율 문제로 인해 리포트가 없는 경우:
  • Array bounds errors
  • Cast exceptions
  • Leaking of tainted data
  • Concurrency race conditions


    • Infer 설치

  • brew 설치를 권장합니다. 벽이 있지만 원본 컴파일링 설치는 상대적으로 고통스럽습니다.
  • brew 설치(2016-11-11은 0.9.2 버전으로 xcode8에서 테스트에 문제가 있음): brew install infer
  • 원본 설치는 공식 문서
    # Checkout Infer,            ，        ，       https://github.com/facebook/infer/releases/download/v0.9.3/infer-osx-v0.9.3.tar.xz
git clone https://github.com/facebook/infer.git
cd infer
# Compile Infer,           ，      ，     
./build-infer.sh clang
# Install Infer into your PATH
export PATH=`pwd`/infer/bin:$PATH
    • 참조

    기본 명령

  • Infer 설치 경로 보기: where infer

    • Hello world Objective-C(단일 파일)

    // Hello.m
#import 

@interface Hello: NSObject
@property NSString* s;
@end

@implementation Hello
NSString* m() {
    Hello* hello = nil;
    return hello->_s;
}
@end
  • 실행 명령: infer -- clang -c Hello.m #clang , 상세한 분석은 공식 입구 문서 참조

    • Hello world iOS(일반 XCode 엔지니어링)

  • Go to the sample iOS app in infer/examples/ios_hello and run Infer on it: infer -- xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator

    • pod식 공사

  • /Users/test/Downloads/infer-osx-v0.9.3/infer/bin/infer -- xcodebuild -workspace Flight.xcworkspace -scheme FlightApp -configuration Debug -sdk iphonesimulator -arch i386

    • References

  • Infer 중국어 소개
  • Infer
  • AutomatorX
  • 호르 논리 중국어 강좌
    • Cloudflare Workers에서 Nuxt3 사용 시도
    백준 1449 - 수리공 항승

    좋은 웹페이지 즐겨찾기

    개발자 우수 사이트 수집

    개발자가 알아야 할 필수 사이트 100선 추천 우리는 당신을 위해 100개의 자주 사용하는 개발자 학습 사이트를 정리했습니다
    best100-homepage