หน้าแรก>ซอร์สโค้ด JSP>หมวดหมู่อื่นๆ
ดาวน์โหลด

SEADSA: การวิเคราะห์จุดเพื่อตรวจสอบ C/C ++ ระดับต่ำ

SeaDsa เป็นจุดรวมของบริบท, สนาม-และอาร์เรย์ที่ไวต่อการวิเคราะห์สำหรับการวิเคราะห์ LLVM BitCode ที่ได้รับแรงบันดาลใจจาก DSA SeaDsa เป็นลำดับของขนาดที่ปรับขนาดได้และแม่นยำกว่า Dsa และการดำเนินการก่อนหน้าของ SeaDsa ด้วยการปรับปรุงการจัดการความไวของบริบทการเพิ่มความไวต่อการไหลบางส่วนและการรับรู้ประเภท

แม้ว่า SeaDsa สามารถวิเคราะห์ BitCode LLVM โดยพลการ แต่ได้รับการปรับแต่งสำหรับใช้ในการตรวจสอบโปรแกรมของโปรแกรม C/C ++ มันสามารถใช้เป็นเครื่องมือแบบสแตนด์อโลนหรือร่วมกับกรอบการตรวจสอบ Seahorn และการวิเคราะห์

สาขานี้รองรับ LLVM 14

ความต้องการ

SeaDsa เขียนใน C ++ และใช้ Boost Library ข้อกำหนดหลักคือ:

  • คอมไพเลอร์ C ++ ที่รองรับ C ++ 14
  • boost> = 1.65
  • LLVM 14

ในการเรียกใช้การทดสอบให้ติดตั้งแพ็คเกจต่อไปนี้:

  • sudo pip install lit OutputCheck
  • sudo easy_install networkx
  • sudo apt-get install libgraphviz-dev
  • sudo easy_install pygraphviz

โครงสร้างโครงการ

  1. โครงสร้างข้อมูลหลักถึงกราฟ Graph Cell และ Node ถูกกำหนดไว้ใน include/Graph.hh และ src/Graph.cc
  2. การวิเคราะห์ ท้องถิ่น อยู่ใน include/Local.hh และ src/DsaLocal.cc
  3. การวิเคราะห์ จากล่างขึ้นบน นั้น include/BottomUp.hh และ src/DsaBottomUp.cc
  4. การวิเคราะห์ จากบนลงล่าง อยู่ใน include/TopDown.hh และ src/DsaTopDown.cc
  5. Cloner โหนด Interprocedural อยู่ใน include/Cloner.hh และ src/Clonner.cc
  6. รหัสการจัดการประเภทอยู่ใน include/FieldType.hh , include/TypeUtils.hh , src/FieldType.cc และ src/TypeUtils.cc
  7. การค้นพบฟังก์ชั่นการจัดสรรอยู่ใน include/AllocWrapInfo.hh และ src/AllocWrapInfo.cc

การรวบรวมและการใช้งาน

มาตรฐานการตรวจสอบโปรแกรม

คำแนะนำเกี่ยวกับการตรวจสอบการตรวจสอบโปรแกรมที่ใช้งานพร้อมกับสูตรสำหรับการสร้างโครงการในโลกแห่งความเป็นจริงและผลลัพธ์ของเราสามารถพบได้ใน TEA-DSA-Extras

การรวมในโครงการ C ++ อื่น ๆ (สำหรับผู้ใช้)

SeaDsa มีสองไดเรกทอรี: include และ src เนื่องจาก SeaDsa วิเคราะห์ LLVM BitCode ไฟล์ส่วนหัวและไลบรารีของ LLVM จะต้องสามารถเข้าถึงได้เมื่อสร้างด้วย SeaDsa

หากโครงการของคุณใช้ cmake คุณเพียงแค่ต้องเพิ่มใน CMakeLists.txt ของโครงการของคุณ txt: 

 include_directories(seadsa/include)
 add_subdirectory(seadsa)

สแตนด์อโลน (สำหรับนักพัฒนา)

หากคุณติดตั้ง llvm-14 บนเครื่องของคุณแล้ว: 

 mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run -DLLVM_DIR=__here_llvm-14__/share/llvm/cmake  ..
cmake --build . --target install

มิฉะนั้น: 

 mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run ..
cmake --build . --target install

เพื่อเรียกใช้การทดสอบ: 

 cmake --build . --target test-sea-dsa

ภาพกราฟหน่วยความจำและกราฟการโทรที่สมบูรณ์

พิจารณาโปรแกรม C ที่เรียกว่า tests/c/simple.c : 

 #include <stdlib.h>

typedef struct S {
  int * * x ;
  int * * y ;  
} S ;

int g ;

int main ( int argc , char * * argv ){

  S s1 , s2 ;

  int * p1 = ( int * ) malloc ( sizeof ( int ));
  int * q1 = ( int * ) malloc ( sizeof ( int ));  
  s1 . x = & p1 ;
  s1 . y = & q1 ;    
  * ( s1 . x ) = & g ;
  
  return 0 ;
}

  1. สร้าง bitcode: 

     clang -O0 -c -emit-llvm -S tests/c/simple.c -o simple.ll

ตัวเลือก -O0 ใช้เพื่อปิดใช้งานการเพิ่มประสิทธิภาพเสียงดัง โดยทั่วไปเป็นความคิดที่ดีที่จะเปิดใช้งานการเพิ่มประสิทธิภาพเสียงดัง อย่างไรก็ตามสำหรับตัวอย่างที่ไม่สำคัญเช่น simple.c , Clang ทำให้ง่ายเกินไปมากเกินไปดังนั้นจะไม่มีการสังเกตไม่มีประโยชน์ ตัวเลือก -c -emit-llvm -S สร้าง bitcode ในรูปแบบที่มนุษย์อ่านได้

  1. เรียกใช้ sea-dsa บน bitcode และพิมพ์กราฟหน่วยความจำเพื่อรูปแบบจุด: 

     seadsa -sea-dsa=butd-cs -sea-dsa-type-aware -sea-dsa-dot  simple.ll

ตัวเลือก -sea-dsa=butd-cs -sea-dsa-type-aware เปิดใช้งานการวิเคราะห์ที่ใช้ในกระดาษ FMCAD'19 ของเรา (ดูการอ้างอิง) คำสั่งนี้จะสร้างไฟล์ FUN.mem.dot สำหรับแต่ละฟังก์ FUN ในโปรแกรม bitcode ในกรณีของเราฟังก์ชั่นเดียวเป็น main และมีไฟล์หนึ่งไฟล์ชื่อ main.mem.dot ไฟล์ถูกสร้างขึ้นในไดเรกทอรีปัจจุบัน หากคุณต้องการจัดเก็บไฟล์ .dot ในไดเรกทอรีอื่น ๆ ให้เพิ่มตัวเลือก -sea-dsa-dot-outdir=DIR DIR

  1. เห็นภาพ main.mem.dot โดยแปลงเป็นไฟล์ pdf : 

     dot -Tpdf main.mem.dot -o main.mem.pdf
 open main.mem.pdf  // replace with you favorite pdf viewer

ตัวอย่างของกราฟหน่วยความจำ

ในโมเดลหน่วยความจำของเราค่าตัวชี้จะถูกแสดงโดย เซลล์ ซึ่งเป็นคู่ของวัตถุหน่วยความจำและชดเชย วัตถุหน่วยความจำจะถูกแสดงเป็นโหนดในกราฟหน่วยความจำ ขอบอยู่ระหว่างเซลล์

แต่ละฟิลด์โหนดแสดงถึงเซลล์ (เช่นชดเชยในโหนด) ตัวอย่างเช่นฟิลด์โหนด <0,i32**> และ <8,i32**> ชี้ไปที่ %6 และ %15 ตามลำดับเป็นสองเซลล์ที่แตกต่างกันจากวัตถุหน่วยความจำเดียวกัน ฟิลด์ <8,i32**> หมายถึงเซลล์ที่ออฟเซ็ต 8 ในวัตถุหน่วยความจำที่สอดคล้องกันและประเภทของมันคือ i32** ขอบสีดำแสดงถึงความสัมพันธ์ระหว่างเซลล์ พวกเขามีป้ายกำกับด้วยตัวเลขที่แสดงถึงการชดเชยในโหนดปลายทาง ขอบสีน้ำเงินเชื่อมต่อพารามิเตอร์อย่างเป็นทางการของฟังก์ชั่นกับเซลล์ ขอบสีม่วงเชื่อมต่อตัวแปรตัวชี้ LLVM กับเซลล์ โหนดสามารถมีเครื่องหมายเช่น S (หน่วยความจำที่จัดสรรสแต็ก), H (หน่วยความจำจัดสรรฮีป), M (หน่วยความจำที่แก้ไขแล้ว), R (หน่วยความจำอ่าน), E (หน่วยความจำที่จัดสรรภายนอก) ฯลฯ หากโหนดเป็นสีแดง ฉลาก {void} ใช้เพื่อแสดงว่าโหนดได้รับการจัดสรร แต่ไม่ได้ใช้งานโดยโปรแกรม

sea-dsa ยังสามารถแก้ไขการโทรทางอ้อมได้ การโทรทางอ้อม คือการโทรที่ Callee ไม่เป็นที่รู้จักแบบคงที่ sea-dsa ระบุ callees ที่เป็นไปได้ทั้งหมดของการโทรทางอ้อมและสร้างกราฟการโทร LLVM เป็นเอาต์พุต

พิจารณาตัวอย่างนี้ใน tests/c/complete_callgraph_5.c : 

 struct class_t ;
typedef int ( * FN_PTR )( struct class_t * , int );
typedef struct class_t {
  FN_PTR m_foo ;
  FN_PTR m_bar ;
} class_t ;

int foo ( class_t * self , int x )
{
  if ( x > 10 ) {
    return self -> m_bar ( self , x + 1 );
  } else
    return x ;
}

int bar ( class_t * self , int y ) {
  if ( y < 100 ) {
    return y + self -> m_foo ( self , 10 );
  } else
    return y - 5 ;
}

int main ( void ) {
  class_t obj ;
  obj . m_foo = & foo ;
  obj . m_bar = & bar ;
  int res ;
  res = obj . m_foo ( & obj , 42 );
  return 0 ;
}

พิมพ์คำสั่ง: 

 clang -c -emit-llvm -S tests/c/complete_callgraph_5.c  -o ex.ll
sea-dsa --sea-dsa-callgraph-dot ex.ll

มันสร้างไฟล์ .dot ที่เรียกว่า callgraph.dot ในไดเรกทอรีปัจจุบัน อีกครั้งไฟล์ .dot สามารถแปลงเป็นไฟล์ .pdf และเปิดด้วยคำสั่ง: 

 dot -Tpdf callgraph.dot -o callgraph.pdf
open callgraph.pdf

ตัวอย่างของกราฟการโทร

sea-dsa ยังสามารถพิมพ์สถิติบางอย่างเกี่ยวกับกระบวนการแก้ไขกราฟการโทร (โปรดทราบว่าคุณต้องโทรไป clang ด้วย -g เพื่อพิมพ์ไฟล์บรรทัดและคอลัมน์): 

 sea-dsa --sea-dsa-callgraph-stats ex.ll


=== Sea-Dsa CallGraph Statistics === 
** Total number of indirect calls 0
** Total number of resolved indirect calls 3

%16 = call i32 %12(%struct.class_t* %13, i32 %15) at tests/c/complete_callgraph_5.c:14:12
RESOLVED
Callees:
  i32 bar(%struct.class_t*,i32)
  
%15 = call i32 %13(%struct.class_t* %14, i32 10) at tests/c/complete_callgraph_5.c:23:16
RESOLVED
Callees:
  i32 foo(%struct.class_t*,i32)
  
%11 = call i32 %10(%struct.class_t* %2, i32 42) at tests/c/complete_callgraph_5.c:36:9
RESOLVED
Callees:
  i32 foo(%struct.class_t*,i32)

การจัดการกับไลบรารี C/C ++ และการโทรภายนอก

ความหมายของตัวชี้ของการโทรภายนอกสามารถกำหนดได้โดยการเขียน wrapper ที่เรียกฟังก์ชั่นใด ๆ เหล่านี้ที่กำหนดไว้ใน seadsa/seadsa.h :

  • extern void seadsa_alias(const void *p, ...);
  • extern void seadsa_collapse(const void *p);
  • extern void seadsa_mk_seq(const void *p, unsigned sz);

seadsa_alias รวมเซลล์ของการโต้แย้งทั้งหมด seadsa_collapse บอกให้ sea-dsa ยุบ (เช่นการสูญเสียความไวของสนาม) เซลล์ที่ชี้ด้วย p และ seadsa_mk_seq บอก sea-dsa ให้ทำเครื่องหมายเป็น ลำดับ โหนดที่ชี้ด้วย sz p

ตัวอย่างเช่นพิจารณา foo โทรภายนอกที่กำหนดดังนี้: 

 extern void* foo(const void*p1, void *p2, void *p3);

สมมติว่าตัวชี้ที่ส่งคืนควรเป็นหนึ่งเดียวกับ p2 แต่ไม่ใช่ p1 นอกจากนี้เราต้องการยุบเซลล์ที่สอดคล้องกับ p3 จากนั้นเราสามารถแทนที่ต้นแบบด้านบนของ foo ด้วยคำจำกัดความต่อไปนี้: 

 #include "seadsa/seadsa.h"
void* foo(const void*p1, void *p2, void*p3) {
	void* r = seadsa_new();
	seadsa_alias(r,p2);
	seadsa_collapse(p3);
	return r;
}

การอ้างอิง

  1. "โมเดลหน่วยความจำที่ไวต่อบริบทสำหรับการตรวจสอบโปรแกรม C/C ++" โดย A. Gurfinkel และ JA Navas ใน sas'17 (กระดาษ) | (สไลด์)

  2. "การวิเคราะห์ตัวชี้แบบรวมโดยไม่ต้องใช้งานมากเกินไป" โดย J. Kuderski, JA Navas และ A. Gurfinkel ใน fmcad'19 (กระดาษ)

ขยาย
ข้อมูลเพิ่มเติม
แอปที่เกี่ยวข้อง
แนะนำสำหรับคุณ
ข้อมูลที่เกี่ยวข้อง ทั้งหมด