#prog #rust #article
Using Kani to Validate Security Boundaries in AWS Firecracker
Thanks to Kani, the Firecracker team was able to verify critical areas of code that were intractable to traditional methods. These include our noisy-neighbor mitigation, a rate limiter, where interactions with the system clock resulted in traditional testing being unreliable, as well as our VirtIO stack, where the interaction with guest memory lead to a state space impossible to cover by other means.
We found 5 bugs in our rate limiter implementation, the most significant one a rounding error that allowed guests to exceed their prescribed I/O bandwidth by up to 0.01% in some cases. Additionally, we found one bug in our VirtIO stack, where a untrusted guest could set up a virtio queue that partially overlapped with the MMIO memory region, resulting in Firecracker crashing on boot. Finally, the debug assertions added to the code under verification allowed us to identify a handful of unit tests which were not set up correctly. These have also been fixed.
Using Kani to Validate Security Boundaries in AWS Firecracker
Thanks to Kani, the Firecracker team was able to verify critical areas of code that were intractable to traditional methods. These include our noisy-neighbor mitigation, a rate limiter, where interactions with the system clock resulted in traditional testing being unreliable, as well as our VirtIO stack, where the interaction with guest memory lead to a state space impossible to cover by other means.
We found 5 bugs in our rate limiter implementation, the most significant one a rounding error that allowed guests to exceed their prescribed I/O bandwidth by up to 0.01% in some cases. Additionally, we found one bug in our VirtIO stack, where a untrusted guest could set up a virtio queue that partially overlapped with the MMIO memory region, resulting in Firecracker crashing on boot. Finally, the debug assertions added to the code under verification allowed us to identify a handful of unit tests which were not set up correctly. These have also been fixed.
Kani Rust Verifier Blog
Using Kani to Validate Security Boundaries in AWS Firecracker
Security assurance is paramount for any system running in the cloud. In order to achieve the highest levels of security, we have applied the Kani model checker to verify safety-critical properties in core components of the Firecracker Virtual Machine Monitor…
👍3🤯2🤡1
Forwarded from Денис Чужой про комедию
Иллюстрирую традиционные ценности
https://twitter.com/kirusha_kras/status/1700882669754626261/photo/1
https://twitter.com/kirusha_kras/status/1700882669754626261/photo/1
💩9😁7👍4🤔2🥴2😢1🤡1
Forwarded from Generative Anton
Шмели могут засыпать внутри цветка, если очень сильно устали в течении дня 💔💔💔
🥰28❤6💔4🤡1
#prog #cpp #video
CppCon 2017: Matt Kulukundis “Designing a Fast, Efficient, Cache-friendly Hash Table, Step by Step”
Про дизайн SwissTable, используемой сейчас в Rust std
CppCon 2017: Matt Kulukundis “Designing a Fast, Efficient, Cache-friendly Hash Table, Step by Step”
Про дизайн SwissTable, используемой сейчас в Rust std
YouTube
CppCon 2017: Matt Kulukundis “Designing a Fast, Efficient, Cache-friendly Hash Table, Step by Step”
https://CppCon.org
—
Presentation Slides, PDFs, Source Code and other presenter materials are available at: https://github.com/CppCon/CppCon2017
—
Hash tables consume a large volume of both compute resources and memory across Google's production system. The…
—
Presentation Slides, PDFs, Source Code and other presenter materials are available at: https://github.com/CppCon/CppCon2017
—
Hash tables consume a large volume of both compute resources and memory across Google's production system. The…
🔥5🤡2
#prog #cpp #article
My Dream C++ Additions
Ожидаемо для этого автора, почти все фичи взяты из Rust. Хотя:
> Explicit self reference instead of implicit this pointer
> Of course, this looks rather similar to Rust’s syntax, but believe it or not, I had this idea long before I learned that Rust does self in this way.
My Dream C++ Additions
Ожидаемо для этого автора, почти все фичи взяты из Rust. Хотя:
> Explicit self reference instead of implicit this pointer
> Of course, this looks rather similar to Rust’s syntax, but believe it or not, I had this idea long before I learned that Rust does self in this way.
The Coded Message
My Dream C++ Additions
UPDATE: I have updated this post to address C++ features that address these issues or have been purported to.
I have long day-dreamed about useful improvements to C++. Some of these are inspired by Rust, but some of these are ideas I already had before I…
I have long day-dreamed about useful improvements to C++. Some of these are inspired by Rust, but some of these are ideas I already had before I…
🤡4❤2❤🔥1👏1
Блог*
#prog #cpp #article My Dream C++ Additions Ожидаемо для этого автора, почти все фичи взяты из Rust. Хотя: > Explicit self reference instead of implicit this pointer > Of course, this looks rather similar to Rust’s syntax, but believe it or not, I had this…
C++ Papercuts
(написано до "My Dream C++ Additions")
My current day job is now again a C++ role. And so, I find myself again focusing in this blog post on the downsides of C++.
Overall, I have found returning to active C++ dev to be exactly what I expected: I still have the skills, and can still be effective in it, but now that I have worked in a more modern programming language with less legacy cruft, the downsides of C++ sting more. <...>
In this blog post, I will focus on the minor problems of C++ that have affected me the most, the little usability papercuts, the petty inconveniences that just waste time. Instead of focusing on comparing them to Rust or other programming languages, I will focus on why they don’t make sense from a C++ point of view, with reference to just C++. <...>
While I am proud of my C++ skills, I am not too proud to appreciate that better technology can render them partially obsolete. I am not too proud to appreciate having features that make it easier. In most cases, it’s not a matter of the programming language doing more work for me, but of C++ creating unnecessary extra make-work, often due to decisions that made sense when they were made, but have long since stopped making sense – don’t get me started on header files!
(написано до "My Dream C++ Additions")
My current day job is now again a C++ role. And so, I find myself again focusing in this blog post on the downsides of C++.
Overall, I have found returning to active C++ dev to be exactly what I expected: I still have the skills, and can still be effective in it, but now that I have worked in a more modern programming language with less legacy cruft, the downsides of C++ sting more. <...>
In this blog post, I will focus on the minor problems of C++ that have affected me the most, the little usability papercuts, the petty inconveniences that just waste time. Instead of focusing on comparing them to Rust or other programming languages, I will focus on why they don’t make sense from a C++ point of view, with reference to just C++. <...>
While I am proud of my C++ skills, I am not too proud to appreciate that better technology can render them partially obsolete. I am not too proud to appreciate having features that make it easier. In most cases, it’s not a matter of the programming language doing more work for me, but of C++ creating unnecessary extra make-work, often due to decisions that made sense when they were made, but have long since stopped making sense – don’t get me started on header files!
The Coded Message
C++ Papercuts
UPDATE: Wow, this post has gotten popular! I’ve written a new post that adds new papercuts combined with concrete suggestions for how C++ could improve, if you are interested. Also, if you want to read more about C++’s deeper-than-papercut issues, I recommend…
👍4🤡2
#prog #rust #article
Давно хотел опубликовать, но что-то руки не доходили.
Walk-Through: Prefix Ranges in Rust, a Surprisingly Deep Dive
Или как сделать из
Давно хотел опубликовать, но что-то руки не доходили.
Walk-Through: Prefix Ranges in Rust, a Surprisingly Deep Dive
Или как сделать из
BTreeMap подобие префиксного дерева через инкрементирование строки в системе счисления по основанию char.The Coded Message
Walk-Through: Prefix Ranges in Rust, a Surprisingly Deep Dive
Update: Arvid Norlander has gone through the trouble of refactoring this code into a crate and publishing it. Thank you, Arvid!
Rust’s BTreeMap and corresponding BTreeSet are excellent, B-tree-based sorted map and key types. The map implements the ergonomic…
Rust’s BTreeMap and corresponding BTreeSet are excellent, B-tree-based sorted map and key types. The map implements the ergonomic…
🤡1
Блог*
#prog #rust Хозяйке на заметку Если вы пишите в своём коде определения, которые должны быть доступны в модулях выше, но не в публичном интерфейсе — пишите на самих определениях и на полях pub(crate). В этом случае компилятор не будет предполагать, что к…
Но проблема у этого подхода тоже есть: в силу того, как сделан cargo test, интеграционные тесты сделаны, как отдельные крейты, которые используют тестируемый как зависимость. Так что или вы не сможете получить доступ к этим полям из тестов (а также бенчмарков), или вам придётся делать поля
pub и терять диагностику, если эти поля только в тестах и используются. А навесить #[cfg] отдельно на видимость нельзя🤡1