Дослідники винайшли спосіб автоматичного перетворення коду C на безпечний Rust
Дослідник Еймерік Фромгерц з компанії Inria та науковий співробітник Джонатан Проценко з Azure Research (Microsoft) винайшли спосіб автоматичного перетворення коду C на безпечний код Rust. Він полягає у створенні підмножини C під назвою Mini-C, яка уникає типових шаблонів C і таких функцій, як арифметика вказівників і неявна змінність. Саме через них код С не можна було перекласти на Rust з дотриманням усіх вимог до безпеки, пише The Register.
У статті під назвою «Compiling C to Safe Rust, Formalized» Фромгерц і Проценко пропонують альтернативу автоматичним схемам перетворення C-to-Rust, які створюють небезпечний Rust.
«Замість того, щоб автоматично перекладати C у його повній загальності на небезпечну версію Rust і намагатися зробити отриманий код безпечнішим, ми націлюємося на дані, аплікативну підмножину C. Тому наш процес перекладу є напівактивним: користувачам, можливо, доведеться виконати мінімальні коригування вихідної програми на C, щоб відповідати підмножині підтримуваних мов. Але наш підхід автоматично створює справді безпечний код Rust», — пояснюють вчені.
Використання Mini-C за допомогою фреймворку компілятора KaRaMeL створює безпечний код Rust із застереженням, що після цього може знадобитися деякий рефакторинг.
Свій метод вчені перевірили на криптографічній бібліотеці HACL* (High-Assurance Crypto Library), яка складається з 80 000 рядків коду C, і на EverParse, перевіреній бібліотеці засобів форматування та серіалізації, яка складається з 1400 рядків C. В обох випадках код Rust продемонстрував такий самий профіль продуктивності, як і оригінальний код C, незважаючи на додавання Pointer metadata і перевірок меж виконання.
Резиденти Дія.City сплатили до бюджету понад 8 млрд грн податків в І кварталі 2025 року.…
У Китаї закликають офісних працівників не працювати надто багато — держава сподівається, що вільний час…
Експерти звертають увагу на тривожну тенденцію: люди все частіше використовують ChatGPT, щоб визначити місцезнаходження, зображене…
Компанія JetBrains випустила нову версію мультимовного середовища розробки IntelliJ IDEA 2025.1. Оновлена IDE отримала численні…
Платформа обміну миттєвими повідомленнями Discord впроваджує функцію перевірки віку за допомогою сканування обличчя. Зараз вона…
Wikipedia намагається захистити себе від тисяч різноманітних ботів-скрейперів, які сканують дані цієї платформи для навчання…