june 2013 update of security papers

a guest Jun 21st, 2013 138 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Alright. Every so often I scoop up papers and throw them in folders. It's been disorganized past year or two. Here's some I've dug up recently, a few older ones i ran into again, and a useful one or two someone might not have seen. Apologize for the formatting: just happened when i was copy/pasting stuff and i had too little time to fix it.
  3. Latest Research
  5. (These I posted before. I think they're all great, ground-up redesign ideas. SecureMe's hardware assistance and SAFE's tagged architecture are similar to stuff Ive proposed here over time. Enough researchers gravitate toward a solution it might be worth extra effort, eh?)
  7. Preliminary design of the SAFE Platform 2011 DeHon et al. (They've since made plenty of progress.See
  9. Part of DARPA Clean Slate. Typing/tagging is applied at hardware word level in processor, with a tag unit running parallel to execution. TPM is included. This combo I like most about project. A "concreteware" layer "wraps hardware into an abstract machine." "Userware" runs on top of it. They use high-level, mostly type-safe language called Breeze for all software. A verifiable subset called Tempest is what they'll do systems programming in. Some of that was probably inspired by Pragmatica Project, House, Habit, etc.
  11. SecureME: A Hardware-Software Approach to
  12. Full System Security (2011) Chhabra et al.
  14. "We propose
  15. SecureME, a hardware-software mechanism that provides
  16. such a secure computing environment. SecureME protects
  17. an application from hardware attacks by using a secure pro-
  18. cessor substrate, and also from the Operating System (OS)
  19. through memory cloaking, permission paging, and system
  20. call protection. Memory cloaking hides data from the OS
  21. but allows the OS to perform regular virtual memory man-
  22. agement functions, such as page initialization, copying, and
  23. swapping. Permission paging extends the OS paging mech-
  24. anism to provide a secure way for two applications to es-
  25. tablish shared pages for inter-process communication. Fi-
  26. nally, system call protection applies spatio-temporal pro-
  27. tection for arguments that are passed between the applica-
  28. tion and the OS. Based on our performance evaluation us-
  29. ing microbenchmarks, single-program workloads, and multi-
  30. programmed workloads, we found that SecureME only adds
  31. a small execution time overhead compared to a fully un-
  32. protected system. Roughly half of the overheads are con-
  33. tributed by the secure processor substrate. SecureME also
  34. incurs a negligible additio "
  36. Bootstrapping Trust in Commodity Computers 2010 Parno
  38. It's basically a detailed look at many TPM use cases, tech's, bootstrappings, etc. Good paper for that as TPM use is going up.
  40. (end of that group of papers)
  42. A High-Performance, Low-Overhead Microarchitecture for Secure Program Execution (2012) Kanuparthi et al.
  44. This is essentially dynamic integrity checks on data within the processor as the system runs. This usually slows things down. Their improvement is to treat the calculations transactionally, with a rollback upon failure. Only for static code. 1.66% performance overhead.
  46. Safe Loading - A Foundation for Secure Execution of Untrusted Programs (2012) Payer et al.
  48. Another nice piece of work from ETH Zurich guys. I regularly check on them b/c they do a lot of practical research. This paper is concerned with issues re. the standard loader ( They combine a secure loader with SFI-style sandboxing.
  50. Dissent in Numbers: Making Strong Anonymity Scale (2012) Wolinsky et al
  52. Navy's CHACS lab is at it again! From abstract: "Dissent derives its
  53. scalability from a client/server architecture, in which
  54. many unreliable clients depend on a smaller and more robust, but administratively decentralized, set of servers. Clients trust only that at least one server in the set is hon-est, but need not know or choose which server to trust.... Further, Dissent’s servers can unilaterally ensure progress, even if clients respond slowly or disconnect at arbitrary times, ensuring robust-ness against client churn, tail latencies, and DoS attacks" Tested with 5,000 participants with relatively low latencies.
  56. Enforcing User-Space Privilege Separation with
  57. Declarative Architectures (2012) Niu and Tan
  59. Uses uPro to seperate software into communicating protection domains. Implemented totally in userspace w/out kernel modifications. Developers use declarative language to describe app's security architecture, sparing them crap like SELinux policies. The "related work" section is nice b/c it has a bunch of other stuff for people to look into, esp SFI-related stuff.
  61. Fides: Selectively Hardening Software Application
  62. Components against Kernel-level or Process-level Malware (2012) Strackx and Piessens
  64. "(1) a run-time security architecture that can efficiently
  65.   protect fine-grained software modules executing on a stan-
  66.     dard operating system, and (2) a compiler that compiles
  67.     standard C source code modules to such protected binary
  68.     modules." Doesn't prevent software vulnerabilities necessarily. Just stops vulnerabilities in one compartment from affecting another arbitrarily and forces communications through certain entry points. (Many papers are doing something like this. It's starting to get redundant haha.)
  71. InkTag: Secure Applications on an Untrusted Operating System
  72. (2013) Hoffman et al
  73. "We introduce paraverification, a technique that
  74. simplifies the InkTag hypervisor by forcing the untrusted operating
  75. system to participate in its own verification. Attribute-based access
  76. control allows trusted applications to create decentralized access
  77. control policies. InkTag is also the first system of its kind to ensure
  78. consistency between secure data and metadata, ensuring recover-
  79. ability in the face of system crashes."
  81. INVISIOS: A Lightweight, Minimally Intrusive Secure
  82. Execution Environment 2012 Arora et al (Booz allen hamilton, intel, princeton and purdue were involved here)
  84. Mainly to be applied to embedded systems and SOC's. Quote: " we propose INVISIOS: a lightweight, minimally intrusive hardware-software architecture to
  85. make the execution of security-critical software invisible to the OS, and hence protected from its vulnerabil-
  86. ities. The INVISIOS software architecture encapsulates the security-critical software into a self-contained
  87. software module. While this module is part of the kernel and is run with kernel-level privileges, its code,
  88. data, and execution are transparent to and protected from the rest of the kernel. The INVISIOS hardware
  89. architecture consists of simple add-on hardware components that are responsible for bootstrapping the se-
  90. cure core, ensuring that it is exercised by applications in only permitted ways, and enforcing the isolation
  91. of its code and data. "
  93. Lessons from VAX/SVS for high-assurance VM systems (2012) Lipner, Jaeger and Zurko
  95. Heck yes! Another look at one of my favorite old Orange Book A1 class designs, the VAX Security Kernel. Paul Karger, a now deceased heavyweight in high assurance, contributed to it. There was already a lessons learned paper on it but this paper has worthwhile extra points.
  97. SAFER PATH: Security Architecture using
  98. Fragmented Execution and Replication for
  99. Protection Against Trojaned Hardware by Beaumont et al
  101. "We protect
  102. the integrity of the computation, the confidentiality of data
  103. being processed and ensure system availability. By combining a
  104. small Trusted Computing Base with Commercial-Off-The-Shelf
  105. processing elements, we are able to protect computation from the
  106. effects of arbitrary Hardware Trojans."
  108. Pasture: Secure Offline Data Access Using Commodity Trusted Hardware
  109. by Kolta et al 2013
  111. "Pasture leverages commodity trusted hardware
  112. to provide two important safety properties: access-
  113. undeniability (a user cannot deny any offline data ac-
  114. cess obtained by his device without failing an audit) and
  115. verifiable-revocation (a user who generates a verifiable
  116. proof of revocation of unaccessed data can never access
  117. that data in the future)."
  119. CRUST: Cryptographic Remote Untrusted Storage without Public Keys
  120.  2012 Geron & Wool
  122. "CRUST is intended to be layered
  123. over insecure network file systems without changing the ex-
  124. isting systems. In our approach, data at rest is kept en-
  125. crypted, and data integrity and access control are provided
  126. by cryptographic means. Our design completely avoids
  127. public-key cryptography operations and uses more effi-
  128. cient symmetric-key alternatives to achieve improved per-
  129. formance. "
  131. A Survey of Virtualization Technologies Focusing on Untrusted Code Execution 2012 Zhao et al
  133. Looks at a bunch of them. Useful since it's a common trend in research.
  136. Declarative, Temporal, and Practical Programming with Capabilities (2013)
  138. Some people here have posted on Capsicum for freebsd. This paper describes capweave: a tool that combines a LLVM-based program with a developer-defined policy to rewrite a program to use Capsicum. Deserves mention b/c it's tech that makes security easy on developers and legacy applications. That's always good.
  140. Memory errors - past present and future 2012 van der veen
  142. This paper was a very good read. Sums up various strategies for attacking software via memory over time. I guess heap spraying and ROP are still my favorites. (Or maybe my old UseCacheAsCovertChannel strategy.)
  144. Practical Control Flow Integrity & Randomization for Binary Executables 2013 Zhang et al.
  146. Nice: "We propose a new practical and realistic protection method
  147. called CCFIR (Compact Control Flow Integrity and Random-
  148. ization), which addresses the main barriers to CFI adoption.
  149. CCFIR collects all legal targets of indirect control-transfer in-
  150. structions, puts them into a dedicated “Springboard section” in
  151. a random order, and then limits indirect transfers to flow only
  152. to them. Using the Springboard section for targets, CCFIR can
  153. validate a target more simply and faster than traditional CFI,
  154. and provide support for on-site target-randomization as well
  155. as better compatibility. Based on these approaches, CCFIR can
  156. stop control-flow hijacking attacks including ROP and return-
  157. into-libc."
  159. An Architecture for Enforcing End-to-End Access Control
  160. Over Web Applications 2010 Hicks et al.
  162. I've done custom browser clients in the past so this peaked my interest. They make it easier by using COTS components. "We
  163. overcome the limitations of traditional MAC systems, imple-
  164. mented solely at the operating system layer, by unifying MAC
  165. enforcement across virtual machine, operating system, network-
  166. ing and application layers. We implement our architecture us-
  167. ing Xen virtual machine management, SELinux at the oper-
  168. ating system layer, labeled IPsec for networking and our own
  169. label-enforcing web browser, called FlowwolF."
  171. Secure multi-execution
  172. through static program transformation:
  173. extended version 2012 Barthe et al.
  175. "In a nutshell, SME enforces security by
  176. running one execution of the program per security level, and by
  177. reinterpreting input/output operations w.r.t. their associated se-
  178. curity level. SME is sound, in the sense that the execution of a
  179. program under SME is non-interfering, and precise, in the sense
  180. that for programs that are non-interfering in the usual sense, the
  181. semantics of a program under SME coincides with its standard se-
  182. mantics. A further virtue of SME is that its core idea is language-
  183. independent; it can be applied to a broad range of languages."
  184. "we develop an alter-
  185. native approach where the e ect of SME is achieved through pro-
  186. gram transformation, without modi cations to the runtime, thus
  187. supporting server-side deployment on the web. We show on an ex-
  188. emplary language with input/output and dynamic code evaluation
  189. (modeled after JavaScript's eval) that our transformation is sound
  190. and precise. The crux of the proof is a simulation between the
  191. execution of the transformed program and the SME execution of
  192. the original program. This proof has been machine-checked using
  193. the Agda proof assistant. We also report on prototype implemen-
  194. tations for a small fragment of Python and a substantial subset of
  195. JavaScript."
  197. A Secure User Interface for Web Applications
  198. Running Under an Untrusted Operating System (2010) Li et al
  199. "In this paper, a secure user interface running under
  200. an untrusted OS is proposed, which is independent of the
  201. OS/applications and has a very small code base size. This secure
  202. user interface attests itself to the remote server and then handles
  203. the sensitive input and output by itself, bypassing the OS kernel
  204. and web applications. It utilizes network software stacks in
  205. the OS, however, the sensitive information is cryptographically
  206. protected before being revealed to the potentially malicious OS.
  207. This ensures the confidentiality and integrity of the sensitive
  208. information. Using this secure user interface, even while running
  209. under untrusted OS/applications, the user’s sensitive input,
  210. private output, and transaction integrity can be protected."
  212. Lessons learned building the caernarvon high-assurance operating system 2011 Karger et al.
  214. A smart card OS built for EAL7 by legend Paul Karger (and a team of others). He died a bit after this. The paper explores the issues, tradeoffs and benefits of their foray into EAL7 software design. Incremental development to sustain a project is the No 1 takeaway here.
  216. Fine-Grained Privilege Separation for Web Applications (2010)  Krishnamurthy et al.
  218. "We present a programming model for building web applications
  219. with security properties that can be confidently verified during a
  220. security review. In our model, applications are divided into iso-
  221. lated, privilege-separated components, enabling rich security poli-
  222. cies to be enforced in a way that can be checked by reviewers. In
  223. our model, the web framework enforces privilege separation and
  224. isolation of web applications by requiring the use of an object-
  225. capability language and providing interfaces that expose limited,
  226. explicitly-specified privileges to application components. This ap-
  227. proach restricts what each component of the application can do and
  228. quarantines buggy or compromised code. It also provides a way to
  229. more safely integrate third-party, less-trusted code into a web appli-
  230. cation. We have implemented a prototype of this model based upon
  231. the Java Servlet framework and used it to build a webmail applica-
  232. tion. "
  234. Small Trusted Primitives for Dependable Systems 2011 Maniatis and Chun
  236. Another for TPM fans. Paper focuses on building security cases on a few trusted (or attested) components.
  238. TrustVisor - efficient TCB reduction and attestation 2010 McCune et al.
  240. From the team that brough you the well-designed SecVisor concept: "We present TrustVisor, a special-purpose hypervisor that
  241. provides code integrity as well as data integrity and secrecy
  242. for selected portions of an application. TrustVisor achieves
  243. a high level of security, first because it can protect sensitive
  244. code at a very fine granularity, and second because it has
  245. a very small code base (only around 6K lines of code) that
  246. makes verification feasible. TrustVisor can also attest the ex-
  247. istence of isolated execution to an external entity. We have
  248. implemented TrustVisor to protect security-sensitive code
  249. blocks while imposing less than 7% overhead on the legacy
  250. OS and its applications in the common case."
  252. Verified Security for Browser Extensions (microsoft) Guha et al.
  254. Who said Microsoft don't innovate? ;) "This paper presents I BEX, a new framework for authoring, analyzing, verifying, and deploying secure browser extensions. Our approach is based on using type-safe, high-level languages to program extensions against an API providing access to a variety of browser features. We propose using Datalog to
  255. specify fine-grained access control and data flow policies to
  256. limit the ways in which an extension can use this API, thus
  257. restricting its privilege over security-sensitive web content and
  258. browser resources. We formalize the semantics of policies in
  259. terms of a safety property on the execution of extensions and
  260. develop a verification methodology that allows us to statically
  261. check extensions for policy compliance. Additionally, we provide
  262. visualization tools to assist with policy analysis, and compilers
  263. to translate extension source code to either .NET bytecode or
  264. JavaScript, facilitating cross-browser deployment of extensions."
  266. Provable Protection of Confidential Data in Microkernel-Based Systems 2011 Dresden Group
  268. For microkernel based TCB's. Paper gives a "budget-enforcing, fixed-priority scheduler that provably eliminates covert timing channels; and sound control-flow-sensitive security type system for low-level operating system code." Demonstrates on virtual memory, L4 IPC, and AES timing attack countermeasure.
  270. CertiKOS: A Certified Kernel for Secure Cloud Computing 2011 Gu et al
  272. "Cer-
  273. tiKOS isolates guest applications not only from each other but from
  274. provider-controlled resource management mechanisms. The ker-
  275. nel’s API gives untrusted, provider-supplied management software
  276. control over allocation and delegation of resources such as memory
  277. and I/O devices, but prohibits management code from accessing a
  278. guest’s memory or other resources while in use, or from interfering
  279. with a guest’s execution except through clean resource revocation.
  280. CertiKOS represents an effort to apply recent advances in certified
  281. software design to a ground-up design of a modular and evolvable
  282. certified kernel. Through machine-checkable proof certificates and
  283. runtime monitoring, CertiKOS aims to offer users the assurance of
  284. correct and leak-free execution of their cloud services."
  286. CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency 2011 INRIA
  288. "We describe ClightTSO, a concurrent extension of CompCert’s Clight in which the TSO-based memory
  289. model of x86 multprocessors is exposed for high-performance code, and CompCertTSO, a formally verified
  290. compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in
  291. Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable
  292. behaviour of the generated assembly code (if it does not run out of memory) is also possible in the source
  293. semantics. We also describe some verified fence-elimination optimisations, integrated into CompCertTSO."
  295. SCION: Scalability, Control, and Isolation On
  296. Next-Generation Networks 2011 Zhang et al.
  298. (Networking answer to Clean Slate?) "We present the first Internet architecture designed
  299. to provide route control, failure isolation, and explicit trust
  300. information for end-to-end communications. SCION separates
  301. ASes into groups of independent routing sub-planes, called trust
  302. domains, which then interconnect to form complete routes. Trust
  303. domains provide natural isolation of routing failures and human
  304. misconfiguration, give endpoints strong control for both inbound
  305. and outbound traffic, provide meaningful and enforceable trust,
  306. and enable scalable routing updates with high path freshness. As
  307. a result, our architecture provides strong resilience and security
  308. properties as an intrinsic consequence of good design princi-
  309. ples, avoiding piecemeal add-on protocols as security patches.
  310. Meanwhile, SCION only assumes that a few top-tier ISPs in
  311. the trust domain are trusted for providing reliable end-to-end
  312. communications, thus achieving a small Trusted Computing Base.
  313. Both our security analysis and evaluation results show that
  314. SCION naturally prevents numerous attacks and provides a high
  315. level of resilience, scalability, control, and isolation."
  317. Data-Provenance Verification For Secure Hosts 2012 Xu et al.
  319. "We define data-
  320. provenance integrity as the security property stating that the source where a piece of data is generated cannot be spoofed or tampered
  321. with. We describe a cryptographic provenance verification approach for ensuring system properties and system-data integrity at
  322. kernel-level. Its two concrete applications are demonstrated in the keystroke integrity verification and malicious traffic detection.
  323. Specifically, we first design and implement an efficient cryptographic protocol that enforces keystroke integrity by utilizing on-chip
  324. Trusted Computing Platform (TPM). The protocol prevents the forgery of fake key events by malware under reasonable assumptions.
  325. Then, we demonstrate our provenance verification approach by realizing a lightweight framework for restricting outbound malware
  326. traffic. This traffic-monitoring framework helps identify network activities of stealthy malware, and lends itself to a powerful personal
  327. firewall for examining all outbound traffic of a host that cannot be bypassed."
  329. (Note: I love it when they say "cannot be bypassed.")
  331. Robust Network Covert Communications Based
  332. on TCP and Enumerative Combinatorics 2012 Luo et al
  334. "In this paper, we show through a new class of timing channels coined as Cloak that it is possible to devise a 100 percent
  335. reliable covert channel and yet offer a much higher data rate (up to an order of magnitude) than the existing timing channels. Cloak is
  336. novel in several aspects. First, Cloak uses the different combinations of N packets sent over X flows in each round to represent a
  337. message. The combinatorial nature of the encoding methods increases the channel capacity largely with (N; X). Second, based on the
  338. well-known 12-fold Way, Cloak offers 10 different encoding and decoding methods, each of which has a unique tradeoff among several
  339. important considerations, such as channel capacity and camouflage capability. Third, the packet transmissions modulated by Cloak
  340. can be carefully crafted to mimic normal TCP flows for evading detection."
  342. Silencing Hardware Backdoors 2011 Waksman & Sethumadhavan
  344. "We present the first solution for disabling digital, design-
  345. level hardware backdoors. The principle is that rather than try
  346. to discover the malicious logic in the design – an extremely
  347. hard problem – we make the backdoor design problem itself
  348. intractable to the attacker. The key idea is to scramble inputs
  349. that are supplied to the hardware units at runtime, making it
  350. infeasible for malicious components to acquire the information
  351. they need to perform malicious actions.
  352. We show that the proposed techniques cover the attack space
  353. of deterministic, digital HDL backdoors, provide probabilistic
  354. security guarantees, and can be applied to a wide variety of
  355. hardware components. Our evaluation with the SPEC 2006
  356. benchmarks shows negligible performance loss (less than 1%
  357. on average) and that our techniques can be integrated into
  358. contemporary microprocessor designs."
  360. Language-Independent Sandboxing of
  361. Just-In-Time Compilation and Self-Modifying Code
  362.  2011 Ansel & Marchenko
  364. Extends SFI to work with JIT and dynamic languages. My first thought was hooking Lua or Stackless python into this. Put that on SeLinux, BSD Capsicum or something. Restricted language subset. That's a hell of a start for a secure enough, but productive, platform. Build everything else in the high level language.
  366. Enhancing Data Trustworthiness
  367. via Assured Digital Signing 2012 Dai
  368. " Specifically, ADS allows a signature verifier to
  369. examine not only a signature’s cryptographic validity but also its system security validity that the private signing key and the signing
  370. function are secure, despite the powerful attack that the signing application program and the general-purpose Operating System (OS)
  371. kernel are malicious. The modular design of ADS makes it application-transparent (i.e., no need to modify the application source code
  372. in order to deploy it) and almost hypervisor-independent (i.e., it can be implemented with any Type I hypervisor). To demonstrate the
  373. feasibility of ADS, we report the implementation and analysis of an Xen-based ADS system."
  375. Nice papers that aren't necessarily new, but I'm including them anyway.
  377. Organically assured and survivable information systems 2004 Boeing
  379. This was one I started to consider a practical how to on secure service creation. They combine MAC on hosts, an embedded firewall appliance for enforcement/monitoring on every connected device, app hardening techniques, network rate limiting, an effecient byzantine tolerance algorithm, a modified Secure Spread toolkit, and use their A1-class SNS Server as a trust anchor for secure forwarding and other stuff. Talk about putting it all together. Now to make a version of this that companies can use and Boeing doesn't own... ;)
  381. Overview of Language-based Security Bibliography (2004) Grossman
  383. Good resource for people looking up publications on language-based security up to that point. Includes C-like languages, HLL's, Proof-carrying code, compiler, info-flow security, runtime tools, and many other specialist types of tech. I guess it's also a good resource for beginners to safe/secure language approaches.
  385. CODESSEAL - Compiler FPGA approach to secure applications by Gelbaru et al.
  387. Join compiler/hardware infrastructure for software protection for fully encrypted execution with both program and data encryptedi n memory. Processor + FPGA-based hardware component for fast crypto, and does code integrity verification, authentication and execution flow protection.
  389. HyperSafe: A Lightweight Approach to Provide Lifetime Hypervisor Control-Flow Integrity Wang And Jiang
  391. Two techniques to protect control flow integrity of existing hypervisors. They test it with Xen and Bitvisor + synthethic exploits.
  393. Secure Embedded Processing through Hardware-assisted
  394. Run-time Monitoring 2005 Arora et al.
  396. "Specifically, we extract properties of an embedded program
  397. through static program analysis, and use them as the bases for enforcing permissible program behavior in real-time as the program executes. We present an architecture for hardware-assisted run-time monitoring, wherein the embedded processor is augmented with a hardware monitor that observes the processor’s dynamic execution trace, checks whether the execution trace falls within the allowed program behavior, and flags any deviations from the expected behavior to trigger appropriate response mechanisms. We present properties that can be used to capture permissibleprogram behavior at different levels of granularity within a program, namely inter-procedural control flow, intra-procedural control flow, and instruction stream integrity. We also present a systematic methodology to design application-specific hardware monitors for any given embedded
  398. program. "
  400. ChipLock: Support for Secure Microarchitectures 2005 Kgil et al.
  402. "We show that security support can be added at
  403. some acceptable cost in area and performance. We
  404. propose a processor extension called ChipLock. It pro-
  405. vides hardware security support for a mostly untrusted
  406. operating system to ensure the integrity and confidenti-
  407. ality of all computational results. ChipLock’s modular
  408. design can be easily integrated into existing hardware
  409. platforms with only slight modification to the operating
  410. system. ChipLock includes a built-in hardware Key
  411. Manager that supports symmetric key assignment, and a
  412. read-only-memory, TrustROM, that executes secure
  413. hardware routines. "
  416. Recovery Oriented Computing - Motivations and Case Studies 2002
  418. Compares different variations of this paradigm. Honestly, the rampant insecurity has made this sound more like a good idea every year. The most basic form IT guys have been doing forever: periodically restore a Windows box to factory condition, install apps, patch it all, and back it up. Maintain backup & periodically restore from it. That's a simple version of ROC.
  420. WebDSL: A Case Study in
  421. Domain-Specific Language Engineering 2008 Visser
  423. It's what it sounds like. Think of Ocsigen, Ur/Web, Opa, Sun's DASL or the typesafe functional web platforms. Combine these ideas with builtin security (a la OWASP security api?) to get what I'm getting at.
  425. The Domain-Specific Approach to High Assurance Development ASN.1 Galois Inc. 2006
  427. I was always a fan of ASN.1 over XML. Well, my variants of it anyway. They were simple enough to describe in a page or two, super-easy to parse, and used little bandwidth. Galois takes it to next level with high assurance ASN.1 implementation.
  431. "Although static systems for programming language based information flow control are
  432. well-studied, few works address runtime security of information flow. Runtime informa-
  433. tion flow control offers distinct advantages in precision and in the ability to support dynam-
  434. ically defined policies. To this end, this thesis develops dynamic techniques to track direct
  435. and indirect flows of information, and secure information leaks due to timing channels, in
  436. higher-order programs.
  437. We formulate two runtime information flow systems: λdeps and λsync . λdeps secures
  438. seq
  439. the direct and indirect flows in programs by tracking the dependencies between the values
  440. flowing across various program points, while λsync decouples the publicly observable timing
  441. seq
  442. behavior of programs from secret data by synchronizing the execution times of timing-
  443. sensitive pieces of codes. Noninterference results are proved for all our systems."
  445. A retrospective on the VAX VMM security kernel 1991 Karger et al.
  447. One of the old A1 class products. Good look into rigorous secure system design that accounts for performance, usability and business practicalities.
  449. Kemmerer's paper on Shared Resource Matrix and his follow up paper here. They mention the most mature and effective ways of hunting them down.
  451. KSOS Looking Back by Tom Perrine in login magazine (just google it)
  453. Describes KSOS, one of the old exemplar designs. Compares its features and security to modern stuff. Accuses many modern groups of reinventing the wheel constantly. Commentary on things. Nice read.
  455. I also need to do a paper update on secure databases. I have old papers on integrating MLS or A1-class systems with untrusted databases/software for this purpose. Then, there's modern stuff like sharding and type-safe language constructs. I think some of this could be combined in a way that meets security and performance goals with high robustness with moderate cost/effort.
RAW Paste Data
Pastebin PRO Autumn Special!
Get 40% OFF on Pastebin PRO accounts!