diff --git a/README.md b/README.md index cdbdca8..5400413 100644 --- a/README.md +++ b/README.md @@ -12,11 +12,9 @@ exogenous functions. For endogenous soundness, safety tags should be correctly discharged at the call site, delegated upward, or transformed into new tags associated with the caller. -While tag checking and enforcement are managed by the [safety-tool] linter, the UI +While tag checking and enforcement are executed by the `safety-tool` linter, the UI simply attaches tags as child nodes to the function-level nodes. -[safety-tool]: https://github.com/Artisan-Lab/tag-std/tree/main/safety-tool - ![](https://github.com/user-attachments/assets/e8e41752-e147-4bd0-8de9-f3bceb5c4e19) The side panels juxtapose tag-derived safety documentation with the original safety @@ -77,6 +75,31 @@ docstrings. ![](https://github.com/user-attachments/assets/bc038c70-f1a6-4e1d-b8aa-d8ae158380b5) +## Explanations + +### Start an unsafe function + +The interface offers multiple ways to locate or navigate to specific functions: +* Global Search: Click the search icon in the top bar to access a complete list of +functions. You can refine the results by filtering for function names or specific tags. +* Module Navigation: Click the navigation icon to toggle the left sidebar. This displays a +module-based tree view, where you can browse and select functions within expanded modules. +* Safety Tag Association: Click the tag icon to view the tag specifications and choose a +function the interested tag is annotated on. +* Quick Start: The tool automatically displays a default unsafe function when you switch +between crates. Current supported crates are core, alloc, std, and ostd (AsterinasOS). + +### Tag-derived documentation + +To ensure reusability, tags are designed as templates for backfilling specific variables. +However, our present annotations in the standard library consists only of tag names +without arguments, resulting in generic and incomplete documentation. You'll find more +readable tag-derived output in the ostd crate, as it utilizes full arguments. + +This difference stems from the standard library's audit predating the creation of +safety-tool, leading to its reliance on JSON manipulation, while AsterinasOS was audited +using attribute syntax and the linter. + ## Build the project Commands to build the UI project: @@ -89,7 +112,10 @@ npm install npm run generate # Start the development server on `http://localhost:3000`: npm run dev -# Locally preview production build: -npm run preview ``` +To collect the data, we implemented a custom rustc driver and a cargo wrapper that extract +API information, such as call graphs and ADT-related functions, into JSON format. The +safety tags are sourced from the `tag-std` project. + +The application is a fully static webpage that fetches data hosted in a GitHub repository. diff --git a/audit.md b/audit.md new file mode 100644 index 0000000..2f14fa1 --- /dev/null +++ b/audit.md @@ -0,0 +1,42 @@ + +# Auditing Code with the UI Tool + +We've built a visualization tool for safety tag analysis, deployed as a fully static +webpage at . + +The tool aids human review of safety tags and unsafe code through visualization, by +orchestrating necessary audit information. + +Tag checking and enforcement are implemented by the `#[safety::(...)]` +attributes and `safety-tool` linter, so they fall outside the current UI's purview. + +We use the unsafe `Vec::set_len` function from the `alloc` crate as the default example. +In this view, `InBound` and `ValidNum` tags are displayed within the caller function node, +while their definitions are rendered in the Safety Property panel. + +The graph interface streamlines the representation of UPG edges, presenting only two +categories: +* Caller-to-callee edges: Callee nodes are situated to the right of the caller nodes, and +unsafe functions are marked with a red background. +* Caller-to-field edges: Each is labeled to specify the access type as either read or +write. + +The call graph features the following node interactions: +* A click on a function node updates the side panels to show its tag-derived +documentation, original documentation, source code, and MIR. + * When a function node is selcted, the name will be rendered as a hyperlink in the + documentation panel, allowing you to drill down and audit that specific unit in greater + detail. +* A click on an ADT or field node opens a window for navigating between functions +identified as compromising exogenous soundness in our paper. + * Our analysis focuses on functions associated with ADTs, specifically those where the + ADT serves as the receiver type of the current method (the caller). This scope + encompasses not only constructors but also functions that manipulate the ADT’s state + through direct field access, arguments, or local variables. + +![](https://github.com/user-attachments/assets/d14ba2cd-fec0-4663-8c3c-0ae10992c1c3) + +![](https://github.com/user-attachments/assets/b7253f2a-7fd3-43bf-96d3-0900d3c7283c) + +The top bar includes a help button that displays the README content and offers a feature +overview. diff --git a/ui/app/assets/css/main.css b/ui/app/assets/css/main.css index 2508502..b4d860b 100644 --- a/ui/app/assets/css/main.css +++ b/ui/app/assets/css/main.css @@ -7,6 +7,13 @@ /* this contains the default theme, these are optional styles */ @import '@vue-flow/core/dist/theme-default.css'; +@theme { + /* unsafe text (bg) */ + --color-unsafe: oklch(0.69 0.25 12.26); + /* unsafe node (bg) */ + --color-unsafe-node: oklch(0.28 0.11 14.75); +} + /* General codeblock styles. */ .shiki, .shiki span { @apply !leading-tight !text-base; @@ -128,7 +135,7 @@ html, body { }; } .upg-node-unsafe-fn { - @apply bg-red-100 dark:bg-red-900/30; + @apply bg-red-100 dark:bg-unsafe-node; } .upg-node-tag { @@ -216,5 +223,5 @@ html, body { .unsafeFnLink { @apply text-rose-700 hover:text-rose-500 font-bold transition-colors - dark:hover:text-rose-400 dark:hover:text-rose-300; + dark:text-unsafe dark:hover:text-rose-300; } diff --git a/ui/app/components/UPG.vue b/ui/app/components/UPG.vue index b0c4fd1..504801a 100644 --- a/ui/app/components/UPG.vue +++ b/ui/app/components/UPG.vue @@ -106,7 +106,7 @@ watch(share, val => { router.push({ query: { item: nodeItem.value, - view: flowOpts.value.view.join(","), + // view: flowOpts.value.view.join(","), up: toPanelStr(upPanel.value), down: toPanelStr(downPanel.value), } diff --git a/ui/app/components/code/AdtPopup.vue b/ui/app/components/code/AdtPopup.vue index 2ce3a01..492cd7f 100644 --- a/ui/app/components/code/AdtPopup.vue +++ b/ui/app/components/code/AdtPopup.vue @@ -143,6 +143,7 @@ const initAdtItem = () => { } const search = ref({ withTags: false, unsafeOnly: false, text: "", page: 1, itemsPerPage: 20 }) +watch(active, () => search.value.page = 1) const items = computed(() => { const tree: TreeItem[] = [] diff --git a/ui/app/components/code/Help.vue b/ui/app/components/code/Help.vue index 758ff8e..3413b5c 100644 --- a/ui/app/components/code/Help.vue +++ b/ui/app/components/code/Help.vue @@ -7,7 +7,7 @@ diff --git a/ui/app/lib/output/adt.ts b/ui/app/lib/output/adt.ts index 86a1ac3..b34fddb 100644 --- a/ui/app/lib/output/adt.ts +++ b/ui/app/lib/output/adt.ts @@ -37,7 +37,7 @@ export function adtDoc(adt: DataAdt) { const field_doc = field.doc ? `: ${field.doc}` : "" doc += `* \`${field.name}\`${field_doc}\n\n` } - doc += `### Adt Doc:\n\n${adt.doc_adt}` + doc += `### ADT Doc:\n\n${adt.doc_adt}` return doc }