KAIST разрабатывает технологию автоматического преобразования языка программирования C в Rust с математически гарантированной правильностью

Корреспондент Гу Бон Хёк

- Исследовательская группа под руководством профессора Рю Сок Ёна из факультета компьютерных наук KAIST

- Привлек внимание на крупнейшей в мире конференции по компьютерным наукам

Обложка ноябрьского выпуска международного научного журнала «CAMC», посвященная результатам данного исследования [Предоставлено KAIST]

Язык программирования C, лежащий в основе ключевых программных обеспечений всего мира, включая операционные системы, достиг пределов своей безопасности.

Корейская исследовательская группа проводит пионерские исследования в области базовых технологий для точного автоматического преобразования в Rust, его потенциального преемника. Они продемонстрировали «математическую точность преобразования», которого не хватало у существующих методов искусственного интеллекта (LLM), и смогли решить проблему безопасности языка C путем его автоматического преобразования в Rust, тем самым представив новое направление и видение будущих исследований в области безопасности программного обеспечения.

9 ноября Корейский институт передовых технологий (KAIST) сообщил, что статья исследовательской группы во главе с профессором Рю Сок Ёном из факультета компьютерных наук попала на обложку ноябрьского номера «CACM», международного научного журнала, издаваемого Ассоциацией вычислительной техники (ACM) - крупнейшей в мире международной организацией в области компьютерных наук.

В этой статье всесторонне освещена технология, разработанная исследовательской группой под руководством профессора Рю Сок Ёна для автоматического преобразования языка программирования C в Rust. Она получила высокую оценку международного исследовательского сообщества за представление технической концепции и академического направления, которым должны следовать аналогичные исследования в будущем.

Пример преобразования языка C в Rust

Язык программирования C широко используется в промышленности с 1970-х годов, но его структурные ограничения постоянно приводят к серьезным ошибкам и уязвимостям в системе безопасности.

В отличие от него, Rust — это безопасный язык программирования, разработанный в 2015 году, который на данный момент используется при разработке операционных систем и веб-браузеров. Он обладает характеристиками, позволяющими обнаруживать и предотвращать ошибки до запуска программы.

В техническом отчете от февраля 2024 года Белый дом США рекомендовал прекратить использование языка C. Управление перспективных исследовательских проектов Министерства обороны США (DARPA) также реализует проект по разработке технологии автоматического преобразования кода C в Rust, четко указав, что Rust является ключевой альтернативой для решения проблем безопасности C.

Исследовательская группа во главе с профессором Рю проактивно подняла вопросы о проблемах безопасности C и важности автоматического преобразования еще до того, как эти движения набрали обороты, постоянно развивая соответствующие базовые технологии.

В мае 2023 года группа представила технологию преобразования мьютекс, необходимую для синхронизации программ, на ICSE, ведущей конференции по программной инженерии. В июне 2024 года они представили технологию преобразования выходных параметров, используемую для передачи результатов, на PLDI, ведущей конференции в области языков программирования. В октябре того же года они представили технологию преобразования объединений (юнионов), которая хранит разнообразные данные вместе, на ASE, ведущей конференции в области автоматизации программного обеспечения.

Профессор Рю Сок Ён (слева) и доктор Хон Чжэ Мин [Предоставлено KAIST]

Все три исследования представляют собой «первые в мире» достижения, представленные на ведущих международных конференциях, которые значительно усовершенствовали реализацию технологий автоматического преобразования для каждой функции.

Исследовательская группа зарекомендовала себя как ведущая команда мирового уровня, которая ежегодно с 2023 года публикует статьи в CACM, последовательно решая важные и сложные проблемы.

«Разработанная нами технология преобразования является фундаментальной технологией, основанной на теории языков программирования, и ее основная сила заключается в возможности доказать «правильность» преобразования» - сказал первый автор статьи доктор Хон Чжэ Мин, добавив: «В то время как большинство исследований опирается на большие языковые модели (LLM), наша технология может математически гарантировать правильность преобразования».

nbgkoo@heraldcorp.com

#южнаякорея #корея #политика #экономика #промышленность #технология #бизнес #финансы #программирование #программныеобепечения #rust #языкипрограммирования #автоматизация #медицина #культура #общество #искусство #азия