From 2fc5a2b25ce365a6fc8b0c6f2cff3f7fdbfbd835 Mon Sep 17 00:00:00 2001 From: zjp Date: Sat, 31 Jan 2026 16:56:32 +0000 Subject: [PATCH 01/11] ui(share): don't emit view route argument because it's not used anymore --- ui/app/components/UPG.vue | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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), } From c6ae215f7128a06a407b77166711a5bda0e52f07 Mon Sep 17 00:00:00 2001 From: zjp Date: Sun, 1 Feb 2026 02:15:50 +0000 Subject: [PATCH 02/11] fix(AdtPopup): reset page number to 1 when tree item switches --- ui/app/components/code/AdtPopup.vue | 1 + 1 file changed, 1 insertion(+) 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[] = [] From 0fce9c0a4773b2e58195af313856f2c0cb58f22f Mon Sep 17 00:00:00 2001 From: zjp Date: Sun, 1 Feb 2026 02:52:42 +0000 Subject: [PATCH 03/11] ui(css): define unsafe and unsafe-node color with OKLCH --- ui/app/assets/css/main.css | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) 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; } From f9d0c5c3ed25254114206835658c0eb221b509cf Mon Sep 17 00:00:00 2001 From: zjp Date: Sun, 1 Feb 2026 03:04:34 +0000 Subject: [PATCH 04/11] README: explain data source --- README.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index cdbdca8..e53e3c1 100644 --- a/README.md +++ b/README.md @@ -89,7 +89,12 @@ 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. + +[tag-std]: https://github.com/safer-rust/tag-std + +The application is a fully static webpage that fetches data hosted in a GitHub repository. From 5250bc1f07fe3d379a1666a85d912108636dba1f Mon Sep 17 00:00:00 2001 From: zjp Date: Sun, 1 Feb 2026 03:16:55 +0000 Subject: [PATCH 05/11] ui(doc): Adt => ADT --- ui/app/lib/output/adt.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 } From a2d5cdc1396f9fcc8ff5bfc38befc69d0148b4a5 Mon Sep 17 00:00:00 2001 From: zjp Date: Sun, 1 Feb 2026 09:11:45 +0000 Subject: [PATCH 06/11] README: add explanations section --- README.md | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/README.md b/README.md index e53e3c1..74306c9 100644 --- a/README.md +++ b/README.md @@ -77,6 +77,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: From 2a28bf8b4806060f1a41d45f95aca6594b6b78cf Mon Sep 17 00:00:00 2001 From: zjp Date: Sun, 1 Feb 2026 09:12:42 +0000 Subject: [PATCH 07/11] doc: add audit md --- audit.md | 45 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 audit.md diff --git a/audit.md b/audit.md new file mode 100644 index 0000000..e8369e6 --- /dev/null +++ b/audit.md @@ -0,0 +1,45 @@ + +# Auditing Code with the UI Tool + +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 visually marked with a red background. +* Caller-to-field edges: Each is labeled to specify the access type as either read or +write. + +The graph interface significantly simplifies the UPG edges. Only two kinds of edge are +presented: +* on the caller-to-callee edge, the caller node starts to the right to the callees; unsafe + functions are in red background +* caller-to-field edges are labelled with access way + +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. + * Specifically, 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. From 5eb4a07a9177737b31b571208ea9672ef2c1a471 Mon Sep 17 00:00:00 2001 From: zjp Date: Sun, 1 Feb 2026 09:44:40 +0000 Subject: [PATCH 08/11] doc: attach deployment URL in audit.md --- audit.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/audit.md b/audit.md index e8369e6..bcab6fd 100644 --- a/audit.md +++ b/audit.md @@ -1,6 +1,9 @@ # 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. From d64b237ffa0901fa43d2414bbfc934ee64a8ee7d Mon Sep 17 00:00:00 2001 From: zjp Date: Sun, 1 Feb 2026 09:51:09 +0000 Subject: [PATCH 09/11] doc: clean up in audit md --- audit.md | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/audit.md b/audit.md index bcab6fd..2f14fa1 100644 --- a/audit.md +++ b/audit.md @@ -17,22 +17,16 @@ 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 visually marked with a red background. +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 graph interface significantly simplifies the UPG edges. Only two kinds of edge are -presented: -* on the caller-to-callee edge, the caller node starts to the right to the callees; unsafe - functions are in red background -* caller-to-field edges are labelled with access way - 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. - * Specifically, 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. + * 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 From b52696f993f9afa60307e65331863e0b98216783 Mon Sep 17 00:00:00 2001 From: zjp Date: Sun, 1 Feb 2026 10:06:14 +0000 Subject: [PATCH 10/11] README: hide links --- README.md | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 74306c9..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 @@ -118,8 +116,6 @@ npm run dev 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. - -[tag-std]: https://github.com/safer-rust/tag-std +safety tags are sourced from the `tag-std` project. The application is a fully static webpage that fetches data hosted in a GitHub repository. From 9bec79122814999fba5b4378fe1a893766c684af Mon Sep 17 00:00:00 2001 From: zjp Date: Sun, 1 Feb 2026 10:06:33 +0000 Subject: [PATCH 11/11] ui(help): update to README --- ui/app/components/code/Help.vue | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) 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 @@