Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities

استفاده از تکنیک های تجزیه و تحلیل استاتیک برای اثبات صحت جزئی کد C اخیراً به دلیل هزینه بالای خطاهای نرم افزار - به ویژه با توجه به آسیب پذیری های امنیتی - توجه زیادی را به خود جلب کرده است. با این حال، تحقیق در مورد تکنیک‌های تحلیل جدید اغلب به دلیل مشکلات فنی تجزیه و تحلیل دسترسی‌ها از طریق اشاره‌گرها، محاسبات نشانگر، اجبار بین انواع، پیچیدن اعداد صحیح و سایر رفتارهای سطح پایین با مشکل مواجه می‌شود. اکسل سایمون یک توصیف مختصر و در عین حال رسمی از یک تجزیه و تحلیل دامنه ارزش ارائه می‌کند که معنایی برنامه‌های C را با استفاده از سیستم‌های نابرابری‌های خطی (چند وجهی) به خوبی تقریب می‌کند.

تحلیل به طور رسمی تا سطح بیت مشخص می‌شود و در عین حال تقریب دقیقی از تمام جنبه‌های سطح پایین C با استفاده از عملیات چند وجهی ارائه می‌کند و به این ترتیب، مبنایی را فراهم می‌کند. برای پیاده سازی تجزیه و تحلیل های جدید که با هدف تأیید دقیق ویژگی های برنامه سطح بالاتر است. یکی از نمونه‌های چنین تحلیلی، ردیابی موقعیت NUL در بافرهای رشته‌ای C است که به‌عنوان توسعه‌ای برای تحلیل پایه نشان داده می‌شود و در نتیجه ماژولار بودن رویکرد را نشان می‌دهد.

در حالی که این کتاب بر تجزیه و تحلیل صحیح زبان C تمرکز دارد، برای هر محقق و دانشجویی که علاقه مند به تجزیه و تحلیل استاتیک زبان های برنامه نویسی دنیای واقعی است مفید خواهد بود. در واقع، بسیاری از مفاهیم ارائه شده در اینجا به زبان های دیگر مانند جاوا یا اسمبلر، به برنامه های کاربردی دیگر مانند تجزیه و تحلیل لکه، تجزیه و تحلیل آرایه و شکل و احتمالاً حتی به رویکردهای دیگر مانند تأیید زمان اجرا و تولید داده های آزمایشی منتقل می شوند.

The use of static analysis techniques to prove the partial correctness of C code has recently attracted much attention due to the high cost of software errors - particularly with respect to security vulnerabilities. However, research into new analysis techniques is often hampered by the technical difficulties of analysing accesses through pointers, pointer arithmetic, coercion between types, integer wrap-around and other low-level behaviour. Axel Simon provides a concise, yet formal description of a value-range analysis that soundly approximates the semantics of C programs using systems of linear inequalities (polyhedra).

The analysis is formally specified down to the bit-level while providing a precise approximation of all low-level aspects of C using polyhedral operations and, as such, it provides a basis for implementing new analyses that are aimed at verifying higher-level program properties precisely. One example of such an analysis is the tracking of the NUL position in C string buffers, which is shown as an extension to the basic analysis and which thereby demonstrates the modularity of the approach.

While the book focuses on a sound analysis of C, it will be useful to any researcher and student with an interest in static analysis of real-world programming languages. In fact, many concepts presented here carry over to other languages such as Java or assembler, to other applications such as taint analysis, array and shape analysis and possibly even to other approaches such as run-time verification and test data generation.