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