消极词汇 发表于 2025-3-30 09:43:36
http://reply.papertrans.cn/88/8711/871026/871026_51.png对手 发表于 2025-3-30 14:46:48
Types and Effects for Non-interfering Program Monitors the sequence of program actions deviates from a specified security policy, the monitor transforms the sequence or terminates the program. We present the design and formal specification of a language for defining the policies enforced by program monitors..Our language provides a number of facilities有危险 发表于 2025-3-30 20:01:43
http://reply.papertrans.cn/88/8711/871026/871026_53.png焦虑 发表于 2025-3-30 23:21:46
Enforcing Java Run-Time Properties Using Bytecode Rewritingodify the semantics of Java while making no changes to the Java virtual machine itself. While this gives us portability and power, there are numerous pitfalls, mostly stemming from the limitations imposed upon Java bytecode by the Java virtual machine. We reflect on our experience building three sec郊外 发表于 2025-3-31 03:35:48
http://reply.papertrans.cn/88/8711/871026/871026_55.pnginsert 发表于 2025-3-31 06:33:50
Formalization and Verification of a Mail Server in Coqgs of the mail server may be abused for eavesdropping mail contents, spreading virus, sending spam messages, etc. We have verified a part of a mail server written in Java, by manually translating the Java program into a Coq function as faithfully as possible, and verifying properties of the Coq funcexigent 发表于 2025-3-31 12:26:51
Design and Implementation of Security System Based on Immune System cooperation among immune cells of the system. This system implements each immune cell as an agent based on our multiagent language, which is an extension of concurrent logic programming languages. These agents can detect and reject intrusion by cooperating with each other.他姓手中拿着 发表于 2025-3-31 16:52:44
http://reply.papertrans.cn/88/8711/871026/871026_58.pngAlveolar-Bone 发表于 2025-3-31 18:54:26
Typing One-to-One and One-to-Many Correspondences in Security Protocolsed to specify correctness properties of cryptographic protocols. In earlier work, we showed how to typecheck one-to-one correspondences for protocols expressed in the spi-calculus. We present a new type and e.ect system able to verify both one-to-one and one-to-many correspondences.Infelicity 发表于 2025-3-31 22:46:55
Proof-Carrying Code with Untrusted Proof RulesPCC the producer negotiates beforehand, and in an unspecified way, with the consumer the permission to prove safety in whatever high-level way it chooses. In practice this has meant that highlevel rules for type safety have been hard-wired into the system as part of the trusted code base. This limit