{"id":120678,"date":"2024-11-24T15:46:00","date_gmt":"2024-11-24T13:46:00","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/inicziativa-po-verifikaczii-standartnoj-biblioteki-rust"},"modified":"2024-11-24T15:46:00","modified_gmt":"2024-11-24T13:46:00","slug":"inicziativa-po-verifikaczii-standartnoj-biblioteki-rust","status":"publish","type":"post","link":"https:\/\/prohoster.info\/en\/blog\/news\/inicziativa-po-verifikaczii-standartnoj-biblioteki-rust","title":{"rendered":"Initiative for verifying the Rust standard library","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Amazon and the Rust Foundation have launched an initiative aimed at enhancing the security of the standard library of the Rust programming language. The goal is to verify the reliability and safety of functions that utilize the keyword 'unsafe', which allows operations that interact unsafely with memory, such as dereferencing pointers, modifying static variables, and accessing external libraries in C\/C++. It is noted that the current standard library of Rust contains approximately 35,000 functions, with 7,500 containing code blocks executed in the context of 'unsafe'. Over the past three years, 57 issues related to functionality have been identified in the library, of which 20 were marked as vulnerabilities. <\/p>\n
The library verification work is organized in the form of a competition, where participants are presented with various tasks related to performing specific checks to confirm safe memory handling with Rust libraries or developing tools for automating such checks. Successful completion of the verification goal (providing formal proof of reliability) involves a reward. A repository has been created for conducting experiments and publishing work results, acting as a branch from the official Rust repository. <\/p>\n
Currently, 13 tasks have been proposed. For instance, one task involves verifying the safety of working with raw pointers in functions from the module core::ptr and providing formal proof of the correctness of pointer operations. Existing tools such as Aeneas, Kani, Gillian, Verus, and Creusot can be used for verification, or new tools can be suggested. Examples of completed tasks. \n Source: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"