{"id":9472,"date":"2024-11-24T11:47:15","date_gmt":"2024-11-24T18:47:15","guid":{"rendered":"https:\/\/jasonsblog.ddns.net\/?p=9472"},"modified":"2024-11-24T11:50:36","modified_gmt":"2024-11-24T18:50:36","slug":"aws-will-pay-devs-to-verify-rust-standard-library-because-of-7500-unsafe-functions-and-enormity-of-task","status":"publish","type":"post","link":"https:\/\/jasonsblog.ddns.net\/index.php\/2024\/11\/24\/aws-will-pay-devs-to-verify-rust-standard-library-because-of-7500-unsafe-functions-and-enormity-of-task\/","title":{"rendered":"AWS Will Pay Devs to Verify Rust Standard Library Because of 7,500 Unsafe Functions and Enormity of Task"},"content":{"rendered":"\n<p>This is interesting as the <a href=\"https:\/\/jasonsblog.ddns.net\/index.php\/2024\/11\/09\/the-us-government-wants-developers-to-stop-using-c-and-c\/\">federal government is trying to persuade coders and contractors to move to Rust and other &#8220;safe&#8221; programming languages<\/a>. Quality coders using C and C++ who do data validation to avoid memory and code execution issues are secure, so it would appear some of these &#8220;safe&#8221; compilers haven&#8217;t quite been vetted for the hype to use them over much more established programming languages and programmers. Of course, the real push is so they don&#8217;t have to pay for experienced programmers and can pick up cheap options right out of school (Mahindra LTD was doing this when I was with AT&amp;T and it was a nightmare and why I left). And I&#8217;d hate to think about what we&#8217;ll get out of supposed AI programming, and fearfully Google admits that 25% of their code is AI generated. Let that sync in.<\/p>\n\n\n\n<p><a href=\"https:\/\/devclass.com\/2024\/11\/21\/aws-will-pay-devs-to-verify-rust-standard-library-because-of-7500-unsafe-functions-and-enormity-of-task\/\" target=\"_blank\" rel=\"noreferrer noopener\">https:\/\/devclass.com\/2024\/11\/21\/aws-will-pay-devs-to-verify-rust-standard-library-because-of-7500-unsafe-functions-and-enormity-of-task\/<\/a><\/p>\n\n\n<div class=\"wp-block-ub-divider ub_divider ub-divider-orientation-horizontal\" id=\"ub_divider_2dde89a3-cb4c-4200-b540-fa93e4674ed1\"><div class=\"ub_divider_wrapper\" style=\"position: relative; margin-bottom: 2px; width: 100%; height: 2px; \" data-divider-alignment=\"center\"><div class=\"ub_divider_line\" style=\"border-top: 2px solid #ccc; margin-top: 2px; \"><\/div><\/div><\/div>\n\n\n<p>By Tim Anderson<\/p>\n\n\n\n<p>AWS, in collaboration with the Rust Foundation, is crowdsourcing an effort to verify the Rust standard library, by setting out a series of challenges for devs and offering financial rewards for solutions.<\/p>\n\n\n\n<p>The safety of the Rust programming language is key to its appeal. Recommendations to switch from C and C++ to Rust have come from a wide range of sources, including the <a href=\"https:\/\/devclass.com\/2024\/02\/27\/white-house-demands-memory-safe-programming-languages-but-iso-c-group-says-its-only-part-of-solution\/\">US government<\/a>, <a href=\"https:\/\/www.theregister.com\/2022\/09\/20\/rust_microsoft_c\/\">Microsoft Azure CTO Mark Russinovich<\/a>, and Rust is now supported for use in the Linux kernel.<\/p>\n\n\n\n<p>Rust includes ways to bypass its safety guarantees though, with the use of the \u201cunsafe\u201d keyword. The documentation <a href=\"https:\/\/doc.rust-lang.org\/book\/ch19-01-unsafe-rust.html\">remarks<\/a> that \u201cIf Rust didn\u2019t let you do unsafe operations, you couldn\u2019t do certain task,\u201d such as directly interacting with the operating system, though it adds that \u201cyou use unsafe Rust at your own risk,\u201d where risks include null pointer dereferencing, a common source of security issues.<\/p>\n\n\n\n<p>The issue AWS <a href=\"https:\/\/aws.amazon.com\/blogs\/opensource\/verify-the-safety-of-the-rust-standard-library\/\">highlights<\/a> is that even if developers use only safe code, most applications still depend on the Rust standard library. AWS states that there are approximately 7.5K unsafe functions in the Rust Standard Library and notes that 57 \u201csoundness issues\u201d and 20 CVEs (Common Vulnerabilities and Exposures) have been reported in the last three years. The cloud giant also claimed that \u201cthe rate of change of the standard libraries is faster and more unsound.\u201d&nbsp;<\/p>\n\n\n\n<p>Marking a function as unsafe does not mean it is vulnerable, only that Rust does not guarantee its safety. AWS plans to reduce the risk by using tools and techniques for formal verification of key library code, but believes that \u201ca single team would be unable to make significant inroads\u201d for reasons including the lack of a verification mechanism in the Rust ecosystem and what it calls the \u201cunknowns of scalable verification.\u201d<\/p>\n\n\n\n<p>The plan therefore is to turn this over to the community, by posing challenges and rewarding developers for solutions. The Rust Foundation is supporting the effort and is <a href=\"https:\/\/foundation.rust-lang.org\/news\/rust-foundation-collaborates-with-aws-initiative-to-verify-rust-standard-libraries\/\">hosting the challenge<\/a>.<\/p>\n\n\n\n<p>A <a href=\"https:\/\/github.com\/model-checking\/verify-rust-std\">GitHub repository<\/a> provides a fork of the Rust code and includes a set of challenges, currently 13 of them. Solutions have to use approved tools (though there is scope to submit a new tool). The <a href=\"https:\/\/model-checking.github.io\/verify-rust-std\/general-rules.html#solution-requirements\">rules<\/a> also state that the solution must not impact the runtime logic of the standard library.<\/p>\n\n\n\n<p>The Rust Foundation says that there is a financial reward tied to each challenge, and that the \u201cchallenge rewards committee is responsible for reviewing activity and dispensing rewards.\u201d How much will be paid though is not stated.<\/p>\n\n\n\n<p>Despite the wide admiration for Rust, there is <a href=\"https:\/\/devclass.com\/2023\/11\/17\/rust-now-has-a-specification-team-but-it-will-not-define-the-language\/\">no formal specification for the language<\/a>, an issue which impacts formal verification efforts.<\/p>\n\n\n\n<p>The <a href=\"https:\/\/model-checking.github.io\/verify-rust-std\/intro.html\">current list of challenges<\/a> is as follows:<\/p>\n\n\n\n<ol class=\"wp-block-list\">\n<li>Verify core transmuting methods<\/li>\n\n\n\n<li>Verify the memory safery of core intrinsics using raw pointers<\/li>\n\n\n\n<li>Verifying Raw Pointer Arithmetic Operations<\/li>\n\n\n\n<li>Memory safety of BTreeMap\u2019s btree::node module<\/li>\n\n\n\n<li>Verify functions iterating over inductive data type: linked_list<\/li>\n\n\n\n<li>Safety of NonNull<\/li>\n\n\n\n<li>Safety of Methods for Atomic Types and ReentrantLock<\/li>\n\n\n\n<li>Contracts for SmallSort<\/li>\n\n\n\n<li>Safe abstractions for core::time::Duration<\/li>\n\n\n\n<li>Memory safety of String<\/li>\n\n\n\n<li>Safety of Methods for Numeric Primitive Types<\/li>\n\n\n\n<li>Safety of NonZero<\/li>\n\n\n\n<li>Safety of CStr<\/li>\n<\/ol>\n","protected":false},"excerpt":{"rendered":"<p>This is interesting as the federal government is trying to persuade coders and contractors to move to Rust and other &#8220;safe&#8221; programming languages. Quality coders using C and C++ who do data validation to avoid memory and code execution issues are secure, so it would appear some of these &#8220;safe&#8221; compilers haven&#8217;t quite been vetted [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[6,7],"tags":[],"class_list":["post-9472","post","type-post","status-publish","format-standard","hentry","category-tech","category-world"],"blocksy_meta":[],"featured_image_src":null,"author_info":{"display_name":"Jason","author_link":"https:\/\/jasonsblog.ddns.net\/index.php\/author\/jturning\/"},"_links":{"self":[{"href":"https:\/\/jasonsblog.ddns.net\/index.php\/wp-json\/wp\/v2\/posts\/9472","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/jasonsblog.ddns.net\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/jasonsblog.ddns.net\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/jasonsblog.ddns.net\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/jasonsblog.ddns.net\/index.php\/wp-json\/wp\/v2\/comments?post=9472"}],"version-history":[{"count":3,"href":"https:\/\/jasonsblog.ddns.net\/index.php\/wp-json\/wp\/v2\/posts\/9472\/revisions"}],"predecessor-version":[{"id":9475,"href":"https:\/\/jasonsblog.ddns.net\/index.php\/wp-json\/wp\/v2\/posts\/9472\/revisions\/9475"}],"wp:attachment":[{"href":"https:\/\/jasonsblog.ddns.net\/index.php\/wp-json\/wp\/v2\/media?parent=9472"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/jasonsblog.ddns.net\/index.php\/wp-json\/wp\/v2\/categories?post=9472"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/jasonsblog.ddns.net\/index.php\/wp-json\/wp\/v2\/tags?post=9472"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}