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

OpenBSD formal driver verification with SeL4

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Nicolae, Adriana Irofti, Paul Leuştean, Ioana LOS-CS-FMI University of Bucharest Romania Institute for Logic and Data Science Romania

The seL4 microkernel is currently the only kernel that has been fully formally verified. In general, the increased interest in ensuring the security of a kernel’s code results from its important role in the entire operating system. One of the basic features of an operating system is that it abstracts the handling of devices. This abstraction is represented by device drivers - the software that manages the hardware. A proper verification of the software component could ensure that the device would work properly unless there is a hardware failure. In this paper, we choose to model the behavior of a device driver and build the proof that the code implementation matches the expected behavior. The proof was written in Isabelle/HOL, the code translation from C to Isabelle was done automatically by the use of the C-to-Isabelle Parser and AutoCorres tools. We choose Isabelle theorem prover because its efficiency was already shown through the verification of seL4 microkernel. Copyright © 2023, The Authors. All rights reserved.

关键词： Formal verification

Pinky: A Modern Malware-oriented Dynamic Information Retrieval Tool

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Irofti, Paul LOS-CS-FMI University of Bucharest Romania Institute for Logic and Data Science Romania

We present here a reverse engineering tool that can be used for information retrieval and anti-malware techniques. Our main contribution is the design and implementation of an instrumentation framework aimed at providing insight on the emulation process. Sample emulation is achieved via translation of the binary code to an intermediate representation followed by compilation and execution. The design makes this a versatile tool that can be used for multiple task such as information retrieval, reverse engineering, debugging, and integration with anti-malware products. Copyright © 2023, The Authors. All rights reserved.

关键词： Information retrieval

Software Mitigation of RISC-V Spectre Attacks

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Bălucea, Ruxandra Irofti, Paul LOS-CS-FMI University of Bucharest Romania Institute for Logic and Data Science Romania

Speculative attacks are still an active threat today that, even if initially focused on the x86 platform, reach across all modern hardware architectures. RISC-V is a newly proposed open instruction set architecture that has seen traction from both the industry and academia in recent years. In this paper we focus on the RISC-V cores where speculation is enabled and, as we show, where Spectre attacks are as effective as on x86. Even though RISC-V hardware mitigations were proposed in the past, they have not yet passed the prototype phase. Instead, we propose low-overhead software mitigations for Spectre-BTI, inspired from those used on the x86 architecture, and for Spectre-RSB, to our knowledge the first such mitigation to be proposed. We show that these mitigations work in practice and that they can be integrated in the LLVM toolchain. For transparency and reproducibility, all our programs and data are made publicly available online. Copyright © 2022, The Authors. All rights reserved.

关键词： Side channel attack

Intuitionistic Propositional logic in Lean

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Trufas, Dafina LOS Faculty of Mathematics and Computer Science University of Bucharest Institute for Logic and Data Science Bucharest Romania

In this paper we present a formalization of Intuitionistic Propositional logic in the Lean proof assistant. Our approach focuses on verifying two completeness proofs for the studied logical system, as well as exploring the relation between the two analyzed semantical paradigms - Kripke and algebraic. In addition, we prove a large number of theorems and derived deduction rules. © 2024, CC BY.

关键词： Computer circuits

Wikipedia Citations: A comprehensive dataset of citations with identifiers extracted from English Wikipedia

学校读者我要写书评

暂无评论

arXiv 2020年

作者： Singh, Harshdeep West, Robert Colavizza, Giovanni Data Science Laboratory EPFL Institute for Logic Language and Computation University of Amsterdam Netherlands

Wikipedia’s contents are based on reliable and published sources. To this date, little is known about what sources Wikipedia relies on, in part because extracting citations and identifying cited sources is challenging. To close this gap, we release Wikipedia Citations, a comprehensive dataset of citations extracted from Wikipedia. A total of 29.3M citations were extracted from 6.1M English Wikipedia articles as of May 2020, and classified as being to books, journal articles or Web contents. We were thus able to extract 4.0M citations to scholarly publications with known identifiers — including DOI, PMC, PMID, and ISBN — and further labeled an extra 261K citations with DOIs from Crossref. As a result, we find that 6.7% of Wikipedia articles cite at least one journal article with an associated DOI. Scientific articles cited from Wikipedia correspond to 3.5% of all articles with a DOI currently indexed in the Web of science. We release all our code to allow the community to extend upon our work and update the dataset in the future. Copyright © 2020, The Authors. All rights reserved.

关键词：

"Vorbeşti Româneşte?" A Recipe to Train Powerful Romanian LLMs with English Instructions

学校读者我要写书评

暂无评论

"Vorbeşti Româneşte?" A Recipe to Train Powerful Romanian...

2024 Conference on Empirical Methods in Natural Language Processing, EMNLP 2024

作者： Masala, Mihai Ilie-Ablachim, Denis C. Dima, Alexandru Corlatescu, Dragos Zavelca, Miruna Olaru, Ovio Terian, Simina Terian, Andrei Leordeanu, Marius Velicu, Horia Popescu, Marius Dascalu, Mihai Rebedea, Traian Institute for Logic and Data Science Bucharest Romania National University of Science and Technology POLITEHNICA Bucharest Romania Simion Stoilow Institute of Mathematics of The Romanian Academy Bucharest Romania University of Bucharest Romania BRD Groupe Societe Generale Romania Lucian Blaga University Sibiu Romania NVIDIA United States

ISBN: (纸本)9798891761681

In recent years, Large Language Models (LLMs) have achieved almost human-like performance on various tasks. While some LLMs have been trained on multilingual data, most of the training data is in English;hence, their performance in English greatly exceeds other languages. To our knowledge, we are the first to collect and translate a large collection of texts, instructions, and benchmarks and train, evaluate, and release open-source LLMs tailored for Romanian. We evaluate our methods on four different categories, including academic benchmarks, MT-Bench (manually translated), and a professionally built historical, cultural, and social benchmark adapted to Romanian. We argue for the usefulness and high performance of RoLLMs by obtaining state-of-the-art results across the board. We publicly release all resources (i.e., data, training and evaluation code, models) to support and encourage research on Romanian LLMs while concurrently creating a generalizable recipe, adequate for other low or less-resourced languages. © 2024 Association for Computational Linguistics.

关键词： Computational linguistics

Energy-Efficient Trajectory Planning with B-Splines and the Schoenberg Quasi-Interpolant 63

学校读者我要写书评

暂无评论

Energy-Efficient Trajectory Planning with B-Splines and the ...

63rd IEEE Conference on Decision and Control, CDC 2024

作者： Marguet, Vincent Stoican, Florin Prodan, Ionela Univ. Grenoble Alpes Grenoble Inp Institute of Engineering and Management Univ. Grenoble Alpes. Lcis ValenceF-26000 France Politehnica University of Bucharest Acse Faculty of Automatic Control and Computers Bucharest Romania Institute for Logic and Data Science Bucharest Romania

ISBN: (纸本)9798350316339

Few studies address the challenge of minimizing energy consumption during trajectory generation, particularly in the context of multicopter dynamics, characterized by strong non-linearity. This paper introduces a novel approach by formulating energy consumption as a function of B-splines control points, enabling comprehensive optimization of total energy expenditure throughout the trajectory. To mitigate the complexity of representation, we leverage the Schoenberg quasi-interpolant, which not only facilitates the solution of the optimization problem but also effectively reduces computational overhead. The approach is validated through two distinct scenarios: a conventional trajectory used in precision agriculture, and a scenario involving more aggressive maneuvers. © 2024 IEEE.

关键词： Trajectories

Linear rates of asymptotic regularity for Halpern-type iterations

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Cheval, Horaţiu Leuştean, Laurenţiu LOS Faculty of Mathematics and Computer Science University of Bucharest Romania Simion Stoilow Institute of Mathematics of the Romanian Academy Romania Institute for Logic and Data Science Bucharest Romania

In this note we apply a lemma due to Sabach and Shtern to compute linear rates of asymptotic regularity for Halpern-type nonlinear iterations studied in optimization and nonlinear *** Codes 47H05, 47H09, 47J25 © ... 详细信息

关键词： Nonlinear analysis

Artistic control over the glitch in AI-generated motion capture

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Knight, Jamal Johnston, Andrew Berry, Adam Animal Logic Academy University of Technology Sydney SydneyNSW Australia Data Science Institute University of Technology Sydney SydneyNSW Australia

Artificial intelligence (AI) models are prevalent today and provide a valuable tool for artists. However, a lesser-known artifact that comes with AI models that is not always discussed is the glitch. Glitches occur for various reasons;sometimes, they are known, and sometimes they are a mystery. Artists who use AI models to generate art might not understand the reason for the glitch but often want to experiment and explore novel ways of augmenting the output of the glitch. This paper discusses some of the questions artists have when leveraging the glitch in AI art production. It explores the unexpected positive outcomes produced by glitches in the specific context of motion capture and performance art. © 2023, CC BY.

关键词： Machine learning