Links table
1 Introduction
2 dance links
3 Rust programming language
4 RAC: Hardware/Software Widely Shared Assurance
Rust 5 and RAR
5.1 Constrained Algorithmic Rust
6 Dancing in Rust links and 6.1 definitions
6.2 Translation to ACL2
6.3 Theories of dance connections
7 related works
8 Conclusion
9 Acknowledgments and references
3 Rust programming language
The Rust programming language has gained significant attention and use as a modern, type-safe, memory-safe, and formally parsable programming language. Google [29] And Amazon [25] They are big Rust users, and Linus Torvalds has commented favorably on the near-term potential of the Rust toolchain for use in Linux kernel development [1]. After spending decades dealing with a never-ending stream of vulnerabilities due to C/C++, they continue to appear at a high rate [24] Despite its use of sophisticated C/C++ parsing tools, Microsoft announced at its BlueHat 2023 developer conference that it has begun rewriting core Windows libraries in Rust [6].
Our interest in Rust stems from its potential as a common hardware/software assurance language. This interest is driven in part by emerging application areas, such as autonomous and semi-autonomous platforms for land, sea, air, and space, which require sophisticated algorithms and data structures, are subject to stringent accreditation/certification, and encourage hardware/software. Co-design methods. (For an unmanned aerial vehicle use case illustrating a formal systems engineering environment based on methods, please refer to [7] [23].) In this paper, we explore the use of Rust as a high-level syntactic language (HLS). [26].
HLS developers define the high-level abstract behavior of a digital system in a way that overlooks hardware design details such as clocking; The HLS toolchain is then responsible for “filling in the details” to produce a Register Transfer Level (RTL) structure that can be used to realize the design in hardware. HLS development is therefore closer to software development than traditional hardware design in hardware description languages (HDLs) such as Verilog or VHDL. Most current HLS languages are a subset of C, for example Mentor Graphics’ C algorithm [21]Or Vivado HLS by Xilinx [31]although other languages are also used, for example OCaml [15]. A Rust-based HLS would provide a single modern, type-safe and memory-safe expression language for both hardware and software implementations, with very high assurance.
For formal methods researchers, Rust offers the opportunity to think about application-level logic written in the deterministic style favored by the industry, but without the tangle of non-constrained pointers of C/C++. Significant progress has been made to this end in recent years, to the point where developers can validate common algorithm and data structure code that uses common terms such as registers, loops, modular integers, and the like, and verified compilers can ensure this. That this code is properly compiled into binary [18]. Particular progress has been made in the area of hardware/software co-design algorithms, where array-supported data structures are common. [10, 11]. (Note: This style of programming also addresses one of Rust’s drawbacks, which is its lack of support for cyclic data structures.)
As a study of the suitability of Rust as an HLS, we formulate a subset of Rust, inspired by the Rusinov Restricted C (RAC) algorithm. [27]which we called Restricted Algorithmic Rust, or RAR [13]. In fact, in our first implementation of the RAR toolchain, we merely “ported” (performed source-to-source translation) the RAR source to RAC. In doing so, we leverage a number of existing hardware/software co-assurance tools with a minimal investment of time and effort. By converting RAR to RAC, we have access to existing HLS compilers (with the help of some simple C preprocessor directives, we are able to generate code for either the Algorithmic C or Vivado HLS toolchains). But more importantly for our research, we take advantage of the RAC-to-ACL2 compiler that Rusinov and his colleagues at Arm have successfully used to verify industrial-strength floating-point devices.
We have implemented several representational algorithms and data structures in RAR, including:
• A set of matrix-backed algebraic data types, previously implemented in RAC (as stated in [10]);
• A large subset of the Monocypher [30] State-of-the-art cipher suite, including XChacha20 encryption/decryption, Poly1305 (RFC 8439), BLAKE2b hash, and X25519 public key cipher [12]; and
• DFA-based JSON lexicon, combined with an LL(1) JSON parser. The JSON parser was also implemented using the Greibach Normal model (previously implemented in RAC, as described in [14]).
The RAR examples created so far are similar to their RAC counterparts in expressiveness, and we consider the RAR versions to be somewhat superior in terms of readability (this is a very subjective assessment).
In this paper, we will describe the development and formal validation of an array-based Double Link List (CDLL) data structure in RAR, including optimization of Dancing Links. Along the way, we’ll introduce the RAR subset of Rust, the RAR toolchain, a CDLL example, and detail ACL2-based verification techniques, as well as the ACL2 books we used in this example. It is hoped that this explanation will convince the reader of the practicality of RAR as a high-assurance hardware/software co-design language, as well as the feasibility of performing full functional validations of RAR code. We will then conclude with related and future work.
