sea dsa

Seadsa: تحليل نقاط للتحقق من مستوى C/C ++ منخفض المستوى

SeaDsa عبارة عن نقاط للتوحيد السياق والمجال وحساسية التوحيد لـ LLVM Bitcode مستوحاة من DSA. SeaDsa هو ترتيب من حيث الحجم أكثر قابلية للتطوير ودقة من Dsa والتنفيذ السابق لـ SeaDsa بفضل تعامل محسّن لحساسية السياق ، وإضافة حساسية التدفق الجزئي ، والوعي النوعي.

على الرغم من أن SeaDsa يمكنه تحليل LLVM Bitcode التعسفي ، فقد تم تصميمه لاستخدامه في التحقق من برامج C/C ++. يمكن استخدامه كأداة مستقلة أو مع إطار التحقق من Seahorn وتحليلاته.

هذا الفرع يدعم LLVM 14.

متطلبات

SeaDsa مكتوب في C ++ ويستخدم مكتبة Boost. المتطلبات الرئيسية هي:

• برنامج التحويل البرمجي 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 .

التجميع والاستخدام

معايير التحقق من البرنامج

يمكن العثور على تعليمات بشأن تشغيل معايير التحقق من البرنامج ، إلى جانب وصفات لبناء مشاريع العالم الحقيقي ونتائجنا ، في Extras Tea-DDSA.

التكامل في مشاريع C ++ الأخرى (للمستخدمين)

SeaDsa يحتوي على دليلين: include و src . نظرًا لأن SeaDsa تقوم بتحليل LLVM Bitcode ، يجب أن تكون ملفات ومكتبات LLVM متاحة عند البناء مع SeaDsa .

إذا كان مشروعك يستخدم cmake ، فأنت بحاجة فقط إلى إضافة CMakeLists.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. توليد الرمز البريطاني:

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

يتم استخدام الخيار -O0 لتعطيل تحسينات clang. بشكل عام ، من الجيد تمكين تحسينات clang. ومع ذلك ، بالنسبة للأمثلة التافهة مثل simple.c ، يبسط Clang الكثير بحيث لا يمكن ملاحظة أي شيء مفيد. الخيارات -c -emit-llvm -S تنشئ bitcode بتنسيق قابل للقراءة الإنسان.

2. قم بتشغيل sea-dsa على رمز Bitcode وطباعة الرسوم البيانية للذاكرة إلى تنسيق DOT:

    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 . يتم إنشاء الملف في الدليل الحالي. إذا كنت ترغب -sea-dsa-dot-outdir=DIR تخزين ملفات .dot في دليل مختلف DIR أضف الخيار-

3. تصور 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 (STACK MEMORY) ، H (Cheap Tivelocate Memory) ، M (ذاكرة معدلة) ، R (ذاكرة قراءة) ، E (الذاكرة المخصصة خارجيًا) ، وما إلى ذلك إذا كانت العقدة حمراء ، فهذا يعني أن التحليل فقد حساسية المجال لتلك العقدة. يتم استخدام التسمية {void} للدلالة على أنه تم تخصيص العقدة ولكن لم يتم استخدامها من قبل البرنامج.

يمكن لـ sea-dsa أيضًا حل المكالمات غير المباشرة. المكالمة غير المباشرة هي مكالمة حيث لا يعرف Callee بشكل ثابت. يحدد sea-dsa جميع العجول الممكنة لمكالمة غير مباشرة وإنشاء رسم بياني لمكالمة 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 ++ والمكالمات الخارجية

يمكن تعريف مؤشر دلالات المكالمات الخارجية عن طريق كتابة غلاف يدعو أي من هذه الوظائف المحددة في 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 لتسوية التسلسل للعقدة التي يشير إليها p بحجم sz .

على سبيل المثال ، ضع في اعتبارك مكالمة خارجية 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. (ورق)