This paper introduces Certis, a powerful framework that addresses the challenges of cloud asset tracking, management, and threat detection in modern cybersecurity landscapes. It enhances asset identification and anoma...This paper introduces Certis, a powerful framework that addresses the challenges of cloud asset tracking, management, and threat detection in modern cybersecurity landscapes. It enhances asset identification and anomaly detection through SSL certificate parsing, cloud service provider integration, and advanced fingerprinting techniques like JARM at the application layer. Current work will focus on cross-layer malicious behavior identification to further enhance its capabilities, including minimizing false positives through AI-based learning techniques. Certis promises to offer a powerful solution for organizations seeking proactive cybersecurity defenses in the face of evolving threats.展开更多
Translation validation was invented in the 90＇s by Pnueli et al. as a technique to formally verify the correctness of code generators. Rather than certifying the code generator or exhaustively qualifying it, translat...Translation validation was invented in the 90＇s by Pnueli et al. as a technique to formally verify the correctness of code generators. Rather than certifying the code generator or exhaustively qualifying it, translation validators attempt to verify that program transformations preserve semantics. In this work, we adopt this approach to formally verify that the clock semantics and data dependence are preserved during the compilation of the Signal compiler. Translation valida- tion is implemented for every compilation phase from the initial phase until the latest phase where the executable code is generated, by proving the transformation in each phase of the compiler preserves the semantics. We represent the clock semantics, the data dependence of a program and its trans- formed counterpart as first-order formulas which are called clock models and synchronous dependence graphs （SDGs）, respectively. We then introduce clock refinement and depen- dence refinement relations which express the preservations of clock semantics and dependence, as a relation on clock mod- els and SDGs, respectively. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.展开更多
复杂系统的协同仿真中需要运行支撑软件RTI(Run Time Infrastructure)来解决异构模型、异构仿真软件间的数据交互的问题.但RTI的TCP/IP通信机制却无法使得HPC(High Performance Computer)的高速网络Infiniband(IB)在仿真中发挥最大的优...复杂系统的协同仿真中需要运行支撑软件RTI(Run Time Infrastructure)来解决异构模型、异构仿真软件间的数据交互的问题.但RTI的TCP/IP通信机制却无法使得HPC(High Performance Computer)的高速网络Infiniband(IB)在仿真中发挥最大的优势.针对这一问题,本文提出在IB网络架构下基于RDMA(Remote Direct Memory Access)通信机制对RTI进行优化,并以开源HLA项目CERTI软件为基础,研制运行在IB网络下的IB-CERTI软件,最后在不同网络环境下进行对比实验,实验结果证明了IB—CERTI软件在仿真通信中的高效性,特别是仿真邦员间的交互数据量越大,越能提高仿真数据传输效率.展开更多
文摘This paper introduces Certis, a powerful framework that addresses the challenges of cloud asset tracking, management, and threat detection in modern cybersecurity landscapes. It enhances asset identification and anomaly detection through SSL certificate parsing, cloud service provider integration, and advanced fingerprinting techniques like JARM at the application layer. Current work will focus on cross-layer malicious behavior identification to further enhance its capabilities, including minimizing false positives through AI-based learning techniques. Certis promises to offer a powerful solution for organizations seeking proactive cybersecurity defenses in the face of evolving threats.
文摘Translation validation was invented in the 90＇s by Pnueli et al. as a technique to formally verify the correctness of code generators. Rather than certifying the code generator or exhaustively qualifying it, translation validators attempt to verify that program transformations preserve semantics. In this work, we adopt this approach to formally verify that the clock semantics and data dependence are preserved during the compilation of the Signal compiler. Translation valida- tion is implemented for every compilation phase from the initial phase until the latest phase where the executable code is generated, by proving the transformation in each phase of the compiler preserves the semantics. We represent the clock semantics, the data dependence of a program and its trans- formed counterpart as first-order formulas which are called clock models and synchronous dependence graphs （SDGs）, respectively. We then introduce clock refinement and depen- dence refinement relations which express the preservations of clock semantics and dependence, as a relation on clock mod- els and SDGs, respectively. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.
文摘复杂系统的协同仿真中需要运行支撑软件RTI(Run Time Infrastructure)来解决异构模型、异构仿真软件间的数据交互的问题.但RTI的TCP/IP通信机制却无法使得HPC(High Performance Computer)的高速网络Infiniband(IB)在仿真中发挥最大的优势.针对这一问题,本文提出在IB网络架构下基于RDMA(Remote Direct Memory Access)通信机制对RTI进行优化,并以开源HLA项目CERTI软件为基础,研制运行在IB网络下的IB-CERTI软件,最后在不同网络环境下进行对比实验,实验结果证明了IB—CERTI软件在仿真通信中的高效性,特别是仿真邦员间的交互数据量越大,越能提高仿真数据传输效率.
