การทดสอบแบบ Concolic ( คำผสมระหว่างconcreteและsymbolicหรือที่รู้จักกันในชื่อdynamic symbolic execution ) เป็น เทคนิค การตรวจสอบซอฟต์แวร์ แบบผสมผสาน ที่ทำการทดสอบเชิงสัญลักษณ์ ซึ่ง เป็นเทคนิคแบบดั้งเดิมที่ถือว่าตัวแปรในโปรแกรมเป็นตัวแปรเชิงสัญลักษณ์ ควบคู่ไปกับการทดสอบแบบ concrete ( การทดสอบกับอินพุตเฉพาะ) การทดสอบเชิงสัญลักษณ์นี้ใช้ร่วมกับตัวพิสูจน์ทฤษฎีบทอัตโนมัติหรือตัวแก้ข้อจำกัดที่ใช้การเขียนโปรแกรมเชิงตรรกะแบบมีข้อจำกัดเพื่อสร้างอินพุตแบบ concrete ใหม่ (กรณีทดสอบ) โดยมีเป้าหมายเพื่อเพิ่มความครอบคลุมของโค้ด ให้สูงสุด จุดเน้นหลักคือการค้นหาข้อบกพร่องในซอฟต์แวร์ที่ใช้งานจริง มากกว่าการพิสูจน์ความถูกต้องของโปรแกรม

คำอธิบายและการอภิปรายเกี่ยวกับแนวคิดนี้ได้ถูกนำเสนอใน "DART: Directed Automated Random Testing" โดย Patrice Godefroid, Nils Klarlund และ Koushik Sen ^{[ 1 ]}บทความ "CUTE: A concolic unit testing engine for C" ^{[ 2 ]}โดย Koushik Sen, Darko Marinov และGul Aghaได้ขยายแนวคิดนี้ไปสู่โครงสร้างข้อมูล และเป็นผู้บัญญัติศัพท์คำว่าconcolic testing เป็นครั้งแรก เครื่องมืออีกตัวหนึ่งชื่อ EGT (เปลี่ยนชื่อเป็น EXE และต่อมาได้รับการปรับปรุงและเปลี่ยนชื่อเป็น KLEE) ซึ่งมีพื้นฐานมาจากแนวคิดที่คล้ายกัน ได้รับการพัฒนาโดยอิสระโดย Cristian Cadar และDawson Englerในปี 2005 และเผยแพร่ในปี 2005 และ 2006 ^{[ 3 ]} PathCrawler ^{[ 4 ] [ 5 ]}เสนอให้ทำการดำเนินการเชิงสัญลักษณ์ตามเส้นทางการดำเนินการที่เฉพาะเจาะจงเป็นครั้งแรก แต่ต่างจาก concolic testing ตรงที่ PathCrawler ไม่ได้ทำให้ข้อจำกัดเชิงสัญลักษณ์ที่ซับซ้อนง่ายขึ้นโดยใช้ค่าที่เฉพาะเจาะจง เครื่องมือเหล่านี้ (DART และ CUTE, EXE) ใช้การทดสอบแบบ concolic ในการทดสอบหน่วยของ โปรแกรม Cและการทดสอบแบบ concolic เดิมทีถูกคิดค้นขึ้นเพื่อเป็นการปรับปรุงแบบ white box เหนือวิธี การทดสอบแบบสุ่ม ที่มีอยู่ เทคนิคนี้ต่อมาได้ถูกนำไปใช้ในการทดสอบ โปรแกรม Java แบบมัลติเธรด ด้วย jCUTE ^{[ 6 ]}และการทดสอบหน่วยของโปรแกรมจากโค้ดที่เรียกใช้งานได้ (เครื่องมือ OSMOSE) ^{[ 7 ]}นอกจากนี้ยังถูกรวมเข้ากับการทดสอบแบบ fuzz และขยายเพื่อตรวจจับปัญหาด้านความปลอดภัยที่สามารถใช้ประโยชน์ได้ในไบนารี x86ขนาดใหญ่โดยSAGE ของMicrosoft Research ^{[ 8 ] [ 9 ]}

แนวทาง concolic ยังสามารถนำไปใช้กับการตรวจสอบแบบจำลองได้ ในตัวตรวจสอบแบบจำลอง concolic ตัวตรวจสอบแบบจำลองจะสำรวจสถานะของแบบจำลองที่แสดงถึงซอฟต์แวร์ที่กำลังตรวจสอบ ในขณะที่จัดเก็บทั้งสถานะที่เป็นรูปธรรมและสถานะเชิงสัญลักษณ์ สถานะเชิงสัญลักษณ์ใช้สำหรับการตรวจสอบคุณสมบัติของซอฟต์แวร์ ในขณะที่สถานะที่เป็นรูปธรรมใช้เพื่อหลีกเลี่ยงการเข้าถึงสถานะที่ไม่สามารถเข้าถึงได้ เครื่องมือหนึ่งดังกล่าวคือ ExpliSAT โดย Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroeningและ Ishai Rabinovitz ^{[ 10 ]}

การนำการทดสอบแบบดั้งเดิมที่ใช้การประมวลผลเชิงสัญลักษณ์มาใช้ จำเป็นต้องมีการพัฒนาตัวแปลเชิงสัญลักษณ์แบบเต็มรูปแบบสำหรับภาษาโปรแกรมนั้นๆ ผู้พัฒนาการทดสอบแบบ Concolic สังเกตเห็นว่า การพัฒนาการประมวลผลเชิงสัญลักษณ์แบบเต็มรูปแบบนั้นสามารถหลีกเลี่ยงได้ หากการประมวลผลเชิงสัญลักษณ์สามารถผสานรวมกับการประมวลผลปกติของโปรแกรมผ่านการใช้เครื่องมือช่วย แนวคิดในการลดความซับซ้อนของการพัฒนาการประมวลผลเชิงสัญลักษณ์นี้เองที่ก่อให้เกิดการทดสอบแบบ Concolic ขึ้นมา

เหตุผลสำคัญประการหนึ่งที่ทำให้การทดสอบแบบ concolic (และโดยทั่วไป การวิเคราะห์โปรแกรมโดยใช้การดำเนินการเชิงสัญลักษณ์) ได้รับความนิยมเพิ่มขึ้นในช่วงทศวรรษนับตั้งแต่มีการนำเสนอครั้งแรกในปี 2005 คือประสิทธิภาพและพลังในการแสดงออกของตัวแก้ปัญหา SMT ที่ดีขึ้นอย่างมาก การพัฒนาทางเทคนิคที่สำคัญที่นำไปสู่การพัฒนาอย่างรวดเร็วของตัวแก้ปัญหา SMT ได้แก่ การผสมผสานทฤษฎี การแก้ปัญหาแบบ lazy การแก้ปัญหา DPLL(T) และการปรับปรุงความเร็วของตัวแก้ปัญหา SAT อย่างมาก ตัวแก้ปัญหา SMT ที่ได้รับการปรับแต่งเป็นพิเศษสำหรับการทดสอบแบบ concolic ได้แก่Z3 , STP, Z3str2 และBoolector

ลองพิจารณาตัวอย่างง่ายๆ ต่อไปนี้ ซึ่งเขียนด้วยภาษาซี:

void f ( int x , int y ) {int z = 2 * y ;ถ้า( x == 100000 ) {ถ้า( x < z ) {assert ( 0 ); /* ข้อผิดพลาด */}}}

การทดสอบแบบสุ่มอย่างง่าย โดยการลองใช้ค่าxและy แบบสุ่ม จะต้องใช้จำนวนการทดสอบที่มากเกินไปจนไม่สามารถทำได้จริงเพื่อจำลองความล้มเหลว

เราเริ่มต้นด้วยการเลือกค่าxและy อย่างสุ่ม เช่นx  =  y  = 1 ในการดำเนินการจริง บรรทัดที่ 2 กำหนดค่าzเป็น 2 และการทดสอบในบรรทัดที่ 3 ล้มเหลวเนื่องจาก 1 ≠ 100000 ในขณะเดียวกัน การดำเนินการเชิงสัญลักษณ์จะดำเนินไปตามเส้นทางเดียวกัน แต่ถือว่าxและyเป็นตัวแปรเชิงสัญลักษณ์ โดยกำหนดค่าzเป็นนิพจน์ 2y และสังเกตว่า เนื่องจากการทดสอบในบรรทัดที่ 3 ล้มเหลว ดังนั้นx ≠ 100000 อสมการนี้เรียกว่าเงื่อนไขเส้นทางและต้องเป็นจริงสำหรับการดำเนินการทั้งหมดที่ดำเนินไปตามเส้นทางการดำเนินการเดียวกันกับการดำเนินการปัจจุบัน

เนื่องจากเราต้องการให้โปรแกรมทำงานตามเส้นทางที่แตกต่างออกไปในการทำงานครั้งต่อไป เราจึงนำเงื่อนไขเส้นทางสุดท้ายที่พบ คือx ≠ 100000 มากลับเครื่องหมาย ทำให้ได้x = 100000 จากนั้นจึงเรียกใช้โปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติเพื่อหาค่าของตัวแปรอินพุตxและyโดยพิจารณาจากชุดค่าตัวแปรเชิงสัญลักษณ์และเงื่อนไขเส้นทางทั้งหมดที่สร้างขึ้นระหว่างการทำงานเชิงสัญลักษณ์ ในกรณีนี้ คำตอบที่ถูกต้องจากโปรแกรมพิสูจน์ทฤษฎีบทอาจเป็นx = 100000, y = 0

เมื่อรันโปรแกรมด้วยข้อมูลป้อนเข้านี้ โปรแกรมจะไปถึงสาขาภายในในบรรทัดที่ 4 ซึ่งจะไม่ถูกเลือกเนื่องจาก 100000 ( x ) ไม่น้อยกว่า 0 ( z = 2y )เงื่อนไขของเส้นทางคือx = 100000 และx ≥ zซึ่งเงื่อนไขหลังถูกกลับค่า ทำให้ได้x < zจากนั้นตัวพิสูจน์ทฤษฎีบทจะมองหาx , yที่สอดคล้อง กับ x = 100000, x < zและz = 2y ตัวอย่างเช่นx = 100000, y = 50001 ข้อมูลป้อนเข้านี้จะนำไปสู่ข้อผิดพลาด

โดยพื้นฐานแล้ว อัลกอริทึมการทดสอบแบบ concolic ทำงานดังนี้:

1. จำแนกตัวแปรชุดหนึ่งเป็นตัวแปรป้อนเข้าตัวแปรเหล่านี้จะถูก treated เป็นตัวแปรเชิงสัญลักษณ์ในระหว่างการประมวลผลเชิงสัญลักษณ์ ส่วนตัวแปรอื่นๆ ทั้งหมดจะถูก treated เป็นค่าที่เป็นรูปธรรม
2. เพิ่มการตรวจสอบโปรแกรมเพื่อให้ทุกการดำเนินการที่อาจส่งผลต่อค่าตัวแปรเชิงสัญลักษณ์หรือเงื่อนไขของเส้นทางถูกบันทึกในไฟล์ติดตาม รวมถึงข้อผิดพลาดใดๆ ที่เกิดขึ้นด้วย
3. เริ่มต้นด้วยการเลือกข้อมูลป้อนเข้าใดๆ ก็ได้
4. เรียกใช้โปรแกรม
5. ทำการจำลองการทำงานของโปรแกรมบนเส้นทางการทำงาน (trace) โดยใช้สัญลักษณ์ เพื่อสร้างชุดข้อจำกัดเชิงสัญลักษณ์ (รวมถึงเงื่อนไขเส้นทาง)
6. ยกเลิกเงื่อนไขเส้นทางสุดท้ายที่ยังไม่ถูกยกเลิก เพื่อไปยังเส้นทางการทำงานใหม่ หากไม่มีเงื่อนไขเส้นทางดังกล่าว อัลกอริทึมจะสิ้นสุดลง
7. เรียกใช้โปรแกรมแก้ปัญหาความสอดคล้องอัตโนมัติกับชุดเงื่อนไขเส้นทางใหม่เพื่อสร้างอินพุตใหม่ หากไม่มีอินพุตใดที่ตรงตามข้อจำกัด ให้กลับไปที่ขั้นตอนที่ 6 เพื่อลองเส้นทางการดำเนินการถัดไป
8. กลับไปที่ขั้นตอนที่ 4

ขั้นตอนข้างต้นมีข้อควรระวังอยู่บ้าง:

• อัลกอริทึมนี้ทำการค้นหาแบบเจาะลึก (depth-first search)บนโครงสร้างต้นไม้ โดยปริยาย ของเส้นทางการทำงานที่เป็นไปได้ ในทางปฏิบัติ โปรแกรมอาจมีโครงสร้างต้นไม้เส้นทางขนาดใหญ่มากหรือไม่มีที่สิ้นสุด ตัวอย่างทั่วไปคือการทดสอบโครงสร้างข้อมูลที่มีขนาดหรือความยาวไม่จำกัด เพื่อป้องกันไม่ให้เสียเวลามากเกินไปกับพื้นที่เล็กๆ ส่วนใดส่วนหนึ่งของโปรแกรม การค้นหาอาจถูกจำกัดความลึก (bounded)
• การประมวลผลเชิงสัญลักษณ์และโปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติมีข้อจำกัดเกี่ยวกับประเภทของข้อจำกัดที่สามารถแสดงและแก้ไขได้ ตัวอย่างเช่น โปรแกรมพิสูจน์ทฤษฎีบทที่ใช้เลขคณิตเชิงเส้นจะไม่สามารถรับมือกับเงื่อนไขเส้นทางที่ไม่เป็นเชิงเส้นxy = 6 ได้ เมื่อใดก็ตามที่เกิดข้อจำกัดดังกล่าว การประมวลผลเชิงสัญลักษณ์อาจแทนที่ด้วยค่าที่เป็นรูปธรรมในปัจจุบันของตัวแปรใดตัวแปรหนึ่งเพื่อลดความซับซ้อนของปัญหา ส่วนสำคัญของการออกแบบระบบทดสอบแบบคอนโคลิกคือการเลือกการแสดงเชิงสัญลักษณ์ที่แม่นยำเพียงพอที่จะแสดงข้อจำกัดที่สนใจ

การวิเคราะห์และการทดสอบโดยใช้การดำเนินการเชิงสัญลักษณ์โดยทั่วไปได้รับความสนใจอย่างมากจากภาคอุตสาหกรรม เครื่องมือเชิงพาณิชย์ที่มีชื่อเสียงที่สุดที่ใช้การดำเนินการเชิงสัญลักษณ์แบบไดนามิก (หรือที่เรียกว่าการทดสอบเชิงสัญลักษณ์) คือเครื่องมือ SAGE จาก Microsoft เครื่องมือ KLEE และ S2E (ซึ่งทั้งคู่เป็นเครื่องมือโอเพนซอร์สและใช้ตัวแก้ข้อจำกัด STP) ถูกใช้งานอย่างแพร่หลายในหลายบริษัท รวมถึง Micro Focus Fortify, NVIDIA และ IBM เทคโนโลยีเหล่านี้ถูกนำไปใช้โดยบริษัทรักษาความปลอดภัยและแฮกเกอร์มากขึ้นเรื่อยๆ เพื่อค้นหาช่องโหว่ด้านความปลอดภัย

การทดสอบ Concolic มีข้อจำกัดหลายประการ:

• หากโปรแกรมแสดงพฤติกรรมที่ไม่แน่นอน อาจเลือกเส้นทางที่แตกต่างจากที่ตั้งใจไว้ ซึ่งอาจนำไปสู่การไม่สิ้นสุดของการค้นหาและการครอบคลุมที่ไม่ดี
• แม้ในโปรแกรมเชิงกำหนด ปัจจัยหลายอย่างก็อาจนำไปสู่การครอบคลุมที่ไม่ดี รวมถึงการแสดงสัญลักษณ์ที่ไม่แม่นยำ การพิสูจน์ทฤษฎีบทที่ไม่สมบูรณ์ และความล้มเหลวในการค้นหาส่วนที่ให้ผลลัพธ์มากที่สุดในโครงสร้างเส้นทางขนาดใหญ่หรืออนันต์
• โปรแกรมที่ผสมผสานสถานะของตัวแปรอย่างละเอียดถี่ถ้วน เช่น ฟังก์ชันพื้นฐานของการเข้ารหัส จะสร้างการแสดงสัญลักษณ์ขนาดใหญ่มากซึ่งไม่สามารถแก้ไขได้ในทางปฏิบัติ ตัวอย่างเช่น เงื่อนไขดังกล่าวif (sha256_hash(input) == 0x12345678) { ... }ต้องการให้ผู้พิสูจน์ทฤษฎีบททำการผกผันSHA-256ซึ่งเป็นปัญหาที่ยังแก้ไม่ตก

• pathcrawler-online.comเป็นเวอร์ชันที่จำกัดของเครื่องมือ PathCrawler ในปัจจุบัน ซึ่งเปิดให้ใช้งานทั่วไปในฐานะเซิร์ฟเวอร์ทดสอบออนไลน์สำหรับการประเมินผลและเพื่อการศึกษา
• jCUTEมีให้ใช้งานในรูปแบบไบนารีภายใต้ใบอนุญาตสำหรับการใช้งานวิจัยเท่านั้นโดย Urbana-Champaign สำหรับJava
• CRESTเป็นโซลูชันโอเพนซอร์สสำหรับCที่มาแทนที่^{[ 11 ]} CUTE ( ใบอนุญาต BSD ที่แก้ไขแล้ว )
• KLEEเป็นโซลูชันโอเพนซอร์สที่สร้างขึ้นบน โครงสร้างพื้นฐานของ LLVM ( ภายใต้ ใบอนุญาต UIUC )
• CATGเป็นโซลูชันโอเพนซอร์สสำหรับJava ( ภาย ใต้ใบอนุญาต BSD )
• Jalangiเป็นเครื่องมือโอเพนซอร์สสำหรับการทดสอบแบบ concolic และการประมวลผลเชิงสัญลักษณ์สำหรับ JavaScript โดยรองรับทั้งจำนวนเต็มและสตริง
• Microsoft Pexซึ่งพัฒนาโดย Microsoft Rise เปิดให้ใช้งานได้ทั่วไปในฐานะเครื่องมือเสริมสำหรับMicrosoft Visual Studio 2010 บน . NET Framework
• Tritonเป็นไลบรารีการประมวลผลแบบ concolic โอเพนซอร์สสำหรับโค้ดไบนารี
• CutErเป็นเครื่องมือทดสอบ concolic แบบโอเพนซอร์สสำหรับภาษาการเขียนโปรแกรมเชิงฟังก์ชัน Erlang
• Owi ^{[ 12 ]}เป็นเอ็นจิ้น concolic แบบโอเพนซอร์สสำหรับC , C ++ , Rust , WebAssemblyและZig

เครื่องมือหลายอย่าง โดยเฉพาะ DART และ SAGE ยังไม่เปิดให้ใช้งานแก่สาธารณะชนทั่วไป อย่างไรก็ตาม โปรดทราบว่า SAGE นั้น "ถูกใช้เป็นประจำทุกวัน" สำหรับการทดสอบความปลอดภัยภายในของ Microsoft ^{[ 13 ]}