检索结果-内蒙古大学图书馆

Research on Microkernel Integrity Semantics Model and Formal Verification

Chinese Journal of Electronics 2025年第1期23卷 43-48页

作者： Zhenjiang Qian Wei Liu Hao Huang State Key Laboratory for Novel Software Technology Nanjing University Nanjing China Department of Computer Science and Technology Nanjing University Nanjing China

Microkernel integrity is an important aspect of security for the whole microkernel system. Many of the research works on microkernel integrity focus on analysis and safeguards against the existing kernel attacks, and security enhancements for the vulnerabilities of system design and implementation aspects. The formal methods for operating system design and verification ensure the system's high level of security. The existing formalization work and research for operating system mainly focus on the code-level verification of program correctness. In this paper, we propose a formal abstraction model of microkernel in order to accurately describe the semantics of every kernel behavior, and achieve the description of the whole kernel. Based on the model we illustrate the microkernel integrity criterions and elaborate on the integrity mechanism. Meanwhile, we formally verify the completeness and consistency between the mechanism and the definition of the microkernel integrity. We use the self-implemented operating system VTOS (Verified trusted operating system) as an example to illustrate the design method for the microkernel integrity.

关键词： Design methodology Semantics Security Personnel Logic Kernel Protection System analysis and design Research and development Formal verification

来源：评论

学校读者我要写书评

暂无评论

DapperFL: Domain Adaptive Federated Learning with Model Fusion Pruning for Edge Devices 38

DapperFL: Domain Adaptive Federated Learning with Model Fusi...

引用

38th Conference on Neural Information Processing Systems, NeurIPS 2024

作者： Jia, Yongzhe Zhang, Xuyun Hu, Hongsheng Choo, Kim-Kwang Raymond Qi, Lianyong Xu, Xiaolong Beheshti, Amin Dou, Wanchun State Key Laboratory for Novel Software Technology Department of Computer Science and Technology Nanjing University China School of Computing Macquarie University Australia School of Information and Physical Sciences University of Newcastle Australia Department of Information Systems and Cyber Security University of Texas San Antonio United States College of Computer Science and Technology China University of Petroleum [East China China School of Computer and Software Nanjing University of Information Science and Technology China

Federated learning (FL) has emerged as a prominent machine learning paradigm in edge computing environments, enabling edge devices to collaboratively optimize a global model without sharing their private data. However, existing FL frameworks suffer from efficacy deterioration due to the system heterogeneity inherent in edge computing, especially in the presence of domain shifts across local data. In this paper, we propose a heterogeneous FL framework DapperFL, to enhance model performance across multiple domains. In DapperFL, we introduce a dedicated Model Fusion Pruning (MFP) module to produce personalized compact local models for clients to address the system heterogeneity challenges. The MFP module prunes local models with fused knowledge obtained from both local and remaining domains, ensuring robustness to domain shifts. Additionally, we design a Domain Adaptive Regularization (DAR) module to further improve the overall performance of DapperFL. The DAR module employs regularization generated by the pruned model, aiming to learn robust representations across domains. Furthermore, we introduce a specific aggregation algorithm for aggregating heterogeneous local models with tailored architectures and weights. We implement DapperFL on a real-world FL platform with heterogeneous clients. Experimental results on benchmark datasets with multiple domains demonstrate that DapperFL outperforms several state-of-the-art FL frameworks by up to 2.28%, while significantly achieving model volume reductions ranging from 20% to 80%. Our code is available at: https://***/jyzgh/DapperFL. © 2024 Neural information processing systems foundation. All rights reserved.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Hashing based Contrastive Learning for Virtual Screening

arXiv

引用

arXiv 2024年

作者： Han, Jin Hong, Yun Li, Wu-Jun National Key Laboratory for Novel Software Technology Department of Computer Science and Technology Nanjing University Nanjing210023 China

Virtual screening (VS) is a critical step in computer-aided drug discovery, aiming to identify molecules that bind to a specific target receptor like protein. Traditional VS methods, such as docking, are often too time-consuming for screening large-scale molecular databases. Recent advances in deep learning have demonstrated that learning vector representations for both proteins and molecules using contrastive learning can outperform traditional docking methods. However, given that target databases often contain billions of molecules, real-valued vector representations adopted by existing methods can still incur significant memory and time costs in VS. To address this problem, in this paper we propose a hashing-based contrastive learning method, called DrugHash, for VS. DrugHash treats VS as a retrieval task that uses efficient binary hash codes for retrieval. In particular, DrugHash designs a simple yet effective hashing strategy to enable end-to-end learning of binary hash codes for both protein and molecule modalities, which can dramatically reduce the memory and time costs with higher accuracy compared with existing methods. Experimental results show that DrugHash can outperform existing methods to achieve state-of-the-art accuracy, with a memory saving of 32× and a speed improvement of 3.5×. Copyright © 2024, The Authors. All rights reserved.

关键词： Contrastive Learning

来源：评论

学校读者我要写书评

暂无评论

Hashing for Protein Structure Similarity Search

arXiv

引用

arXiv 2024年

作者： Han, Jin Li, Wu-Jun National Key Laboratory for Novel Software Technology Department of Computer Science and Technology Nanjing University Nanjing210023 China

Protein structure similarity search (PSSS), which tries to search proteins with similar structures, plays a crucial role across diverse domains from drug design to protein function prediction and molecular evolution. Traditional alignment-based PSSS methods, which directly calculate alignment on the protein structures, are highly time-consuming with high memory cost. Recently, alignment-free methods, which represent protein structures as fixed-length real-valued vectors, are proposed for PSSS. Although these methods have lower time and memory cost than alignment-based methods, their time and memory cost is still too high for large-scale PSSS, and their accuracy is unsatisfactory. In this paper, we propose a novel method, called protein structure hashing (POSH), for PSSS. POSH learns a binary vector representation for each protein structure, which can dramatically reduce the time and memory cost for PSSS compared with real-valued vector representation based methods. Furthermore, in POSH we also propose expressive hand-crafted features and a structure encoder to well model both node and edge interactions in proteins. Experimental results on real datasets show that POSH can outperform other methods to achieve state-of-the-art accuracy. Furthermore, POSH achieves a memory saving of more than six times and speed improvement of more than four times, compared with other methods. © 2024, CC BY.

关键词： Molecular docking

来源：评论

学校读者我要写书评

暂无评论

AoI-aware Incentive Mechanism for Mobile Crowdsensing using Stackelberg Game 42

AoI-aware Incentive Mechanism for Mobile Crowdsensing using ...

引用

42nd IEEE International Conference on computer Communications, INFOCOM 2023

作者： Xiao, Mingjun Xu, Yin Zhou, Jinrui Wu, Jie Zhang, Sheng Zheng, Jun University of Science and Technology of China School of Computer Science and Technology China Suzhou Institute for Advanced Research University of Science and Technology of China China Temple Universityy Department of Computer and Information Sciences United States Nanjing University State Key Laboratory for Novel Software Technology China

ISBN: (纸本)9798350334142

Mobile CrowdSensing (MCS) is a mobile computing paradigm, through which a platform can coordinate a crowd of workers to accomplish large-scale data collection tasks using their mobile devices. Information freshness has attracted much focus on MCS research worldwide. In this paper, we investigate the incentive mechanism design in MCS systems that take the freshness of collected data and social benefits into concerns. First, we introduce the Age of Information (AoI) metric to measure the freshness of data. Then, we model the incentive mechanism design with AoI guarantees as a novel incomplete information two-stage Stackelberg game with multiple constraints. Next, we derive the optimal strategies of this game so as to determine the optimal reward paid by the platform and the optimal data update frequency for each worker. Moreover, we prove that these optimal strategies form a unique Stackelberg equilibrium. Based on the optimal strategies, we propose an AoI-Aware Incentive (AIAI) mechanism for the MCS system, whereby the platform and all workers can maximize their utilities simultaneously. Meanwhile, the system can ensure that the AoI values of all data uploaded to the platform are not larger than a given threshold to achieve high data freshness. Extensive simulations on real-world traces are conducted to demonstrate the significant performance of AIAI. © 2023 IEEE.

关键词： Optimal systems

来源：评论

学校读者我要写书评

暂无评论

NumLLM: Numeric-Sensitive Large Language Model for Chinese Finance

arXiv

引用

arXiv 2024年

作者： Su, Huan-Yi Wu, Ke Huang, Yu-Hao Li, Wu-Jun National Key Laboratory for Novel Software Technology Department of Computer Science and Technology Nanjing University Nanjing210023 China

Recently, many works have proposed various financial large language models (FinLLMs) by pre-training from scratch or fine-tuning open-sourced LLMs on financial corpora. However, existing FinLLMs exhibit unsatisfactory performance in understanding financial text when numeric variables are involved in questions. In this paper, we propose a novel LLM, called numeric-sensitive large language model (NumLLM), for Chinese finance. We first construct a financial corpus from financial textbooks which is essential for improving numeric capability of LLMs during fine-tuning. After that, we train two individual low-rank adaptation (LoRA) modules by fine-tuning on our constructed financial corpus. One module is for adapting general-purpose LLMs to financial domain, and the other module is for enhancing the ability of NumLLM to understand financial text with numeric variables. Lastly, we merge the two LoRA modules into the foundation model to obtain NumLLM for inference. Experiments on financial question-answering benchmark show that NumLLM can boost the performance of the foundation model and can achieve the best overall performance compared to all baselines, on both numeric and non-numeric questions. Copyright © 2024, The Authors. All rights reserved.

关键词： Finance

来源：评论

学校读者我要写书评

暂无评论

On interleaving space exploration of multi-threaded programs

引用

Frontiers of computer science 2021年第4期15卷 17-28页

作者： Dongjie CHEN Yanyan JIANG Chang XU Xiaoxing MA State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China

Exploring the interleaving space of a multithreaded program to efficiently detect concurrency bugs is important but also difficult because of the astronomically many thread *** paper presents a novel framework to decompose a thread schedule generator that explores the interleaving space into the composition of a basic generator and its extension under the“small interleaving hypothesis”.Under this framework,we in-depth analyzed research work on interleaving space exploration,illustrated how to design an effective schedule generator,and shed light on future research opportunities.

关键词： survey testing concurrency bugs interleaving space

来源：评论

学校读者我要写书评

暂无评论

Hallu-PI: Evaluating Hallucination in Multi-modal Large Language Models within Perturbed Inputs 24

Hallu-PI: Evaluating Hallucination in Multi-modal Large Lang...

引用

32nd ACM International Conference on Multimedia, MM 2024

作者： Ding, Peng Wu, Jingyu Kuang, Jun Ma, Dan Cao, Xuezhi Cai, Xunliang Chen, Shi Chen, Jiajun Huang, Shujian National Key Laboratory for Novel Software Technology Nanjing University Nanjing China College of Computer Science and Technology Zhejiang University Hangzhou China Meituan Shanghai China Meituan Beijing China Zhejiang-Singapore Innovation and AI Joint Research Lab Zhejiang University Hangzhou China

ISBN: (纸本)9798400706868

Multi-modal Large Language Models (MLLMs) have demonstrated remarkable performance on various visual-language understanding and generation tasks. However, MLLMs occasionally generate content inconsistent with the given images, which is known as "hallucination". Prior works primarily center on evaluating hallucination using standard, unperturbed benchmarks, which overlook the prevalent occurrence of perturbed inputs in real-world scenarios-such as image cropping or blurring-that are critical for a comprehensive assessment of MLLMs' hallucination. In this paper, to bridge this gap, we propose Hallu-PI, the first benchmark designed to evaluate Hallucination in MLLMs within Perturbed Inputs. Specifically, Hallu-PI consists of seven perturbed scenarios, containing 1,260 perturbed images from 11 object types. Each image is accompanied by detailed annotations, which include fine-grained hallucination types, such as existence, attribute, and relation. We equip these annotations with a rich set of questions, making Hallu-PI suitable for both discriminative and generative tasks. Extensive experiments on 12 mainstream MLLMs, such as GPT-4V and Gemini-Pro Vision, demonstrate that these models exhibit significant hallucinations on Hallu-PI, which is not observed in unperturbed scenarios. Furthermore, our research reveals a severe bias in MLLMs' ability to handle different types of hallucinations. We also design two baselines specifically for perturbed scenarios, namely Perturbed-Reminder and Perturbed-ICL. We hope that our study will bring researchers' attention to the limitations of MLLMs when dealing with perturbed inputs, and spur further investigations to address this issue. Our code and datasets are publicly available at https://***/NJUNLP/Hallu-PI. © 2024 ACM.

关键词： Visual languages

来源：评论

学校读者我要写书评

暂无评论

Evolution of Web API Cooperation Network via Exploring Community Structure and Popularity

IEEE Transactions on Artificial Intelligence

引用

IEEE Transactions on Artificial Intelligence 2024年第12期5卷 6659-6671页

作者： Kang, Guosheng Wang, Yang Liu, Jianxun Cao, Buqing Xiao, Yong Xu, Yu Hunan University of Science and Technology Hunan Provincial Key Laboratory for Services Computing and Novel Software Technology School of Computer Science and Engineering Xiangtan411201 China University of Cambridge Cambridge Baker Systems Genomics Initiative British Heart Foundation Cardiovascular Epidemiology Unit Department of Public Health and Primary Care CambridgeCB1 8RN United Kingdom

With the growing popularity of the Internet, Web applications have become increasingly essential in our daily lives. Web application programming interfaces (Web APIs) play a crucial role in facilitating interaction between applications. However, most Web service platforms are suffering from the imbalance of Web services now, many services of good quality but low popularity are difficult to be invoked even once and do not create direct connections with the users. Some graph-based Web service recommendation methods also often present a long-tailed distribution of recommended Web services due to limited Mashup-API invocation relationships. To relieve this problem and promote service recommendation, in this article, we propose a community structure and popularity-based approach by constructing an evolving cooperation network for Web APIs. We leverage the Louvain algorithm in community detection to assign community structure to each Web API and consider both the popularity and community structure in constructing the network. By optimizing the Barabαsi-Albert (BA) evolving network model, we demonstrate that our approach outperforms the BA, Bianconi-Barabαsi (BB), and popularity-similarity optimization (PSO) models in Web service clustering. Based on our proposed evolutionary network model for the evolutionary extension of API cooperation network and used for downstream Web service recommendation tasks, the experimental results also show that our recommended approach outperforms some other baseline models for Web service recommendation. © 2020 IEEE.

关键词： Web services

来源：评论

学校读者我要写书评

暂无评论

Verifying Contextual Refinement with Ownership Transfer

引用

Journal of computer science & technology 2021年第6期36卷 1342-1366页

作者： Zhao-Hui Li Xin-Yu Feng School of Computer Science and Technology University of Science and Technology of ChinaHefei 230026China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China

Contextual refinement is a compositional approach to compositional verification of concurrent *** has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract ***,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and *** this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership *** also design a program logic to verify contextual refinement of concurrent objects *** abstract *** have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.

关键词： contextual refinement program logic concurrent object ownership transfer verification

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：