Published April 12, 2024 | Version v1
Publication Open

SpecBCFuzz: Fuzzing LTL Solvers with Boundary Conditions

Creators

  • 1. University of Luxembourg

Description

LTL solvers check the satisfiability of Linear-time Temporal Logic (LTL) formulas and are widely used for verifying and testing critical software systems. Thus, potential bugs in the solvers' implementations can have a significant impact. We present SpecBCFuzz, a fuzzing method for finding bugs in LTL solvers, that is guided by boundary conditions (BCs), corner cases whose (un)satisfiability depends on rare traces. SpecBCFuzz implements a search-based algorithm that fuzzes LTL formulas giving relevance to BCs. It integrates syntactic and semantic similarity metrics to explore the vicinity of the seeded formulas with BCs. We evaluate SpecBCFuzz on 21 different configurations (including the latest and past releases) of four mature and state-of-the-art LTL solvers (NuSMV, Black, Aalta, and PLTL) that implement a diverse set of satisfiability algorithms. SpecBCFuzz produces 368,716 bug-triggering formulas, detecting bugs in 18 out of the 21 solvers' configurations we study. Overall, SpecBCFuzz reveals: soundness issues (wrong answers given by a solver) in Aalta and PLTL; crashes, e.g., segmentation faults, in NuSMV, Black and Aalta; flaky behaviors (different responses across re-runs of the solver on the same formula) in NuSMV and Aalta; performance bugs (large time performance degradation between successive versions of the solver on the same formula) in Black, Aalta and PLTL; and no bug in NuSMV BDD (all versions), suggesting that the latter is currently the most robust solver.

⚠️ This is an automatic machine translation with an accuracy of 90-95%

Translated Description (Arabic)

يتحقق حلالو LTL من مدى ملاءمة صيغ المنطق الزمني للوقت الخطي (LTL) وتستخدم على نطاق واسع للتحقق من أنظمة البرامج الهامة واختبارها. وبالتالي، يمكن أن يكون للأخطاء المحتملة في تطبيقات المحللين تأثير كبير. نقدم SpecBCFuzz، وهي طريقة غامضة للعثور على الأخطاء في محللي LTL، والتي تسترشد بالظروف الحدودية (BCs)، وهي حالات الزاوية التي تعتمد قابليتها للإرضاء (غير) على آثار نادرة. تنفذ SpecBCFuzz خوارزمية قائمة على البحث تحجب صيغ LTL التي تعطي أهمية لـ BCs. فهو يدمج مقاييس التشابه النحوي والدلالي لاستكشاف محيط الصيغ المصنفة مع BCs. نقوم بتقييم SpecBCFuzz على 21 تكوينًا مختلفًا (بما في ذلك الإصدارات الأخيرة والسابقة) لأربعة أجهزة حل LTL ناضجة ومتطورة (NuSMV و Black و Aalta و PLTL) التي تنفذ مجموعة متنوعة من خوارزميات الرضا. تنتج SpecBCFuzz 368،716 تركيبة تحريك الأخطاء، واكتشاف الأخطاء في 18 من أصل 21 تكوينًا للحلالين ندرسها. بشكل عام، يكشف SpecBCFuzz: مشكلات السلامة (الإجابات الخاطئة التي يقدمها المحلل) في Aalta و PLTL ؛ الأعطال، على سبيل المثال، أخطاء التجزئة، في NuSMV و Black و Aalta ؛ السلوكيات المتقشرة (استجابات مختلفة عبر إعادة تشغيل المحلل على نفس الصيغة) في NuSMV و Aalta ؛ أخطاء الأداء (تدهور الأداء لفترة طويلة بين الإصدارات المتعاقبة من المحلل على نفس الصيغة) في Black و Aalta و PLTL ؛ ولا يوجد خلل في NuSMV BDD (جميع الإصدارات)، مما يشير إلى أن الأخير هو حاليًا أقوى محلل.

Translated Description (French)

Les solveurs LTL vérifient la satisfaction des formules de logique temporelle à temps linéaire (LTL) et sont largement utilisés pour vérifier et tester les systèmes logiciels critiques. Ainsi, les bugs potentiels dans les implémentations des solveurs peuvent avoir un impact significatif. Nous présentons SpecBCFuzz, une méthode de fuzzing pour trouver des bogues dans les solveurs LTL, qui est guidée par des conditions aux limites (BC), des cas d'angle dont la (insatisfiabilité) dépend de traces rares. SpecBCFuzz met en œuvre un algorithme basé sur la recherche qui floue les formules LTL donnant de la pertinence aux BC. Il intègre des métriques de similarité syntaxique et sémantique pour explorer le voisinage des formules ensemencées avec les BC. Nous évaluons SpecBCFuzz sur 21 configurations différentes (y compris les versions les plus récentes et passées) de quatre solveurs LTL matures et à la pointe de la technologie (NuSMV, Black, Aalta et PLTL) qui mettent en œuvre un ensemble diversifié d'algorithmes de satisfaction. SpecBCFuzz produit 368 716 formules de déclenchement de bogues, détectant les bogues dans 18 des 21 configurations de solveurs que nous étudions. Dans l'ensemble, SpecBCFuzz révèle : des problèmes de solidité (mauvaises réponses données par un solveur) dans Aalta et PLTL ; des pannes, par exemple des défauts de segmentation, dans NuSMV, Black et Aalta ; des comportements floconneux (réponses différentes lors des réexécutions du solveur sur la même formule) dans NuSMV et Aalta ; des bogues de performance (dégradation des performances en temps important entre les versions successives du solveur sur la même formule) dans Black, Aalta et PLTL ; et aucun bogue dans NuSMV BDD (toutes les versions), ce qui suggère que ce dernier est actuellement le solveur le plus robuste.

Translated Description (Spanish)

Los solucionadores LTL comprueban la satisfacción de las fórmulas de Lógica Temporal de Tiempo Lineal (LTL) y son ampliamente utilizados para verificar y probar sistemas de software críticos. Por lo tanto, los errores potenciales en las implementaciones de los solucionadores pueden tener un impacto significativo. Presentamos SpecBCFuzz, un método de fuzzing para encontrar errores en solucionadores LTL, que se guía por condiciones de límite (BC), casos de esquina cuya (ins)satisfactibilidad depende de rastros raros. SpecBCFuzz implementa un algoritmo basado en la búsqueda que difumina las fórmulas LTL que dan relevancia a las BC. Integra métricas de similitud sintáctica y semántica para explorar las cercanías de las fórmulas sembradas con BC. Evaluamos SpecBCFuzz en 21 configuraciones diferentes (incluidas las versiones más recientes y pasadas) de cuatro solucionadores LTL maduros y de última generación (NuSMV, Black, Aalta y PLTL) que implementan un conjunto diverso de algoritmos de satisfacción. SpecBCFuzz produce 368 716 fórmulas de activación de errores, detectando errores en 18 de las 21 configuraciones de solucionadores que estudiamos. En general, SpecBCFuzz revela: problemas de solidez (respuestas incorrectas dadas por un solucionador) en Aalta y PLTL; fallas, por ejemplo, fallas de segmentación, en NuSMV, Black y Aalta; comportamientos escamosos (diferentes respuestas a través de repeticiones del solucionador en la misma fórmula) en NuSMV y Aalta; errores de rendimiento (degradación del rendimiento a largo plazo entre versiones sucesivas del solucionador en la misma fórmula) en Black, Aalta y PLTL; y ningún error en NuSMV BDD (todas las versiones), lo que sugiere que este último es actualmente el solucionador más robusto.

Files

3597503.3639087.pdf

Files (1.5 MB)

⚠️ Please wait a few minutes before your translated files are ready ⚠️ Note: Some files might be protected thus translations might not work.
Name Size Download all
md5:28b88e18f9d0d0b9778cebedc065694c
1.5 MB
Preview Download

Additional details

Additional titles

Translated title (Arabic)
SpecBCFuzz: تركيب حلالين LTL بشروط حدودية
Translated title (French)
SpecBCFuzz : Résolveurs LTL flous avec des conditions limites
Translated title (Spanish)
SpecBCFuzz: Fuzzing LTL Solvers with Boundary Conditions

Identifiers

Other
https://openalex.org/W4394745232
DOI
10.1145/3597503.3639087

Is supplement to
https://openalex.org/W4312622265 (Other)
https://openalex.org/W4298153058 (Other)
https://openalex.org/W4284708843 (Other)
https://openalex.org/W3176904788 (Other)
https://openalex.org/W2963044240 (Other)
https://openalex.org/W2408080066 (Other)
https://openalex.org/W2268872489 (Other)
https://openalex.org/W21597398 (Other)
https://openalex.org/W2014111643 (Other)
https://openalex.org/W1913543287 (Other)

GreSIS Basics Section

Is Global South Knowledge
Yes
Country
Argentina

References

  • https://openalex.org/W1480909796
  • https://openalex.org/W1489391022
  • https://openalex.org/W1504504841
  • https://openalex.org/W1506588809
  • https://openalex.org/W1512310098
  • https://openalex.org/W1518705996
  • https://openalex.org/W1527982431
  • https://openalex.org/W1539868891
  • https://openalex.org/W1541238879
  • https://openalex.org/W1542807718
  • https://openalex.org/W1554387452
  • https://openalex.org/W1605798759
  • https://openalex.org/W1752393975
  • https://openalex.org/W1819209966
  • https://openalex.org/W182632105
  • https://openalex.org/W1977166502
  • https://openalex.org/W1988808695
  • https://openalex.org/W2002934700
  • https://openalex.org/W2022485595
  • https://openalex.org/W2069709605
  • https://openalex.org/W2076054478
  • https://openalex.org/W2114768982
  • https://openalex.org/W2129289644
  • https://openalex.org/W2138428785
  • https://openalex.org/W2161253570
  • https://openalex.org/W2166280160
  • https://openalex.org/W2171627300
  • https://openalex.org/W221832247
  • https://openalex.org/W2513840768
  • https://openalex.org/W2568050379
  • https://openalex.org/W2613534458
  • https://openalex.org/W2747329762
  • https://openalex.org/W2766540688
  • https://openalex.org/W2777430404
  • https://openalex.org/W2795192724
  • https://openalex.org/W2883887424
  • https://openalex.org/W2888499192
  • https://openalex.org/W2892537867
  • https://openalex.org/W2928427891
  • https://openalex.org/W2962200727
  • https://openalex.org/W3004482543
  • https://openalex.org/W3101588017
  • https://openalex.org/W3102086861
  • https://openalex.org/W3104402823
  • https://openalex.org/W3120742815
  • https://openalex.org/W3149985185
  • https://openalex.org/W3160296189
  • https://openalex.org/W3163844163
  • https://openalex.org/W3181528482
  • https://openalex.org/W4213079124
  • https://openalex.org/W4225922019
  • https://openalex.org/W4232255413
  • https://openalex.org/W4284708843
  • https://openalex.org/W4302764791
  • https://openalex.org/W4308641890
  • https://openalex.org/W4317033095
  • https://openalex.org/W4366196510
  • https://openalex.org/W4366450538
  • https://openalex.org/W4384302760
  • https://openalex.org/W68069235
  • https://openalex.org/W71772184
  • https://openalex.org/W82353766