“تعامل بین اجزای نرم افزار توسط مشخصات پروتکل و فرمت کنترل می شود. متأسفانه، اکثر اسناد مشخصات، متون پیچیدهای هستند که به زبان انگلیسی نوشته شدهاند و باید به صورت دستی به پیادهسازی نرمافزار ترجمه شوند، و جایی برای خطای انسانی باقی میگذارد. “خطاهای منطقی و نقص های مهم اغلب با استفاده گسترده از زبان های برنامه نویسی ناامن به خوبی کاهش می یابند که منجر به آسیب پذیری های امنیتی شدید می شود. با RecordFlux، هدف ما ارائه راهحلی است که با خودکارسازی تولید کد قابل اثبات، در زمان و هزینه صرفهجویی میکند و در عین حال از عدم وجود آسیبپذیریهای سطح پایین مانند سرریز بافر که مهاجمان میتوانند از آن سوء استفاده کنند، اطمینان حاصل کنیم.
AdaCore، ارائهدهنده ابزارهای توسعه و تأیید نرمافزار، امروز از راهاندازی فناوری جدید RecordFlux خود خبر داد که برای تسهیل توسعه و امنیت پروتکلهای ارتباط باینری طراحی شده است. این فناوری شامل یک زبان خاص دامنه (DSL) برای توصیف دقیق فرمتهای پیچیده دادههای باینری و پروتکلهای ارتباطی، و مجموعه ابزاری برای تأیید مشخصات و تولید کد SPARK قابل اثبات است که میتواند بر روی یک CPU هدف اجرا شود.
برای اطلاعات بیشتر به www.adacore.com/recordflux.