Article

Nickel: a framework for design and verification of information flow control systems

Authors:

Helgi Sigurbjarnarson,

Bruno Castro-Karney,

James Bornholt,

Xi WangAuthors Info & Claims

OSDI'18: Proceedings of the 13th USENIX conference on Operating Systems Design and Implementation

Pages 287 - 305

Published: 08 October 2018 Publication History

Abstract

Nickel is a framework that helps developers design and verify information flow control systems by systematically eliminating covert channels inherent in the interface, which can be exploited to circumvent the enforcement of information flow policies. Nickel provides a formulation of noninterference amenable to automated verification, allowing developers to specify an intended policy of permitted information flows. It invokes the Z3 SMT solver to verify that both an interface specification and an implementation satisfy noninterference with respect to the policy; if verification fails, it generates counterexamples to illustrate covert channels that cause the violation.

Using Nickel, we have designed, implemented, and verified NiStar, the first OS kernel for decentralized information flow control that provides (1) a precise specification for its interface, (2) a formal proof that the interface specification is free of covert channels, and (3) a formal proof that the implementation preserves noninterference. We have also applied Nickel to verify isolation in a small OS kernel, NiKOS, and reproduce known covert channels in the ARINC 653 avionics standard. Our experience shows that Nickel is effective in identifying and ruling out covert channels, and that it can verify noninterference for systems with a low proof burden.

References

[1]

ARINC653. Avionics application software standard interface: Part 1, required services, August 2015.

[2]

David E. Bell and Leonard La Padula. Secure computer system: Unified exposition and Multics interpretation. Technical Report MTR-2997, Rev. 1, MITRE Corp., Bedford, MA, March 1976.

[3]

Kenneth J. Biba. Integrity considerations for secure computer systems. Technical Report MTR-3153, MITRE Corp., Bedford, MA, April 1977.

[4]

Alan C. Bomberger, A. Peri Frantz, William S. Frantz, Ann C. Hardy, Norman Hardy, Charles R. Landau, and Jonathan S. Shapiro. The KeyKOS nanokernel architecture. In Proceedings of the USENIX Workshop on Micro-Kernels and Other Kernel Architectures, pages 95-112, April 1992.

Digital Library

[5]

Jo Van Bulck, Marina Minkin, Ofir Weisse, Daniel Genkin, Baris Kasikci, Frank Piessens, Mark Silberstein, Thomas F. Wenisch, Yuval Yarom, and Raoul Strackx. Foreshadow: Extracting the keys to the Intel SGX kingdom with transient out-of-order execution. In Proceedings of the 27th USENIX Security Symposium, pages 991-1008, Baltimore, MD, August 2018.

Digital Library

[6]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 209-224, San Diego, CA, December 2008.

Digital Library

[7]

Winnie Cheng, Dan R. K. Ports, David Schultz, Victoria Popic, Aaron Blankstein, James Cowling, Dorothy Curtis, Liuba Shrira, and Barbara Liskov. Abstractions for usable information flow control in Aeolus. In Proceedings of the 2012 USENIX Annual Technical Conference, Boston, MA, June 2012.

Digital Library

[8]

Andy Chou, Junfeng Yang, Benjamin Chelf, Seth Hallem, and Dawson Engler. An empirical study of operating systems errors. In Proceedings of the 18th ACM Symposium on Operating Systems Principles (SOSP), pages 73-88, Chateau Lake Louise, Banff, Canada, October 2001.

Digital Library

[9]

Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, and Eddy Westbrook. Continuous formal verification of Amazon s2n. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV), pages 430- 446, Oxford, United Kingdom, July 2018.

[10]

David Costanzo, Zhong Shao, and Ronghui Gu. End-to-end verification of information-flow security for C and assembly programs. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 648-664, Santa Barbara, CA, June 2016.

Digital Library

[11]

Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337-340, Budapest, Hungary, March-April 2008.

Digital Library

[12]

Dorothy E. Denning. A lattice model of secure information flow. Communications of the ACM, 19 (5):236-243, May 1976.

Digital Library

[13]

Adam Dunkels. Design and implementation of the lwIP TCP/IP stack. Swedish Institute of Computer Science, February 2001.

[14]

Petros Efstathopoulos and Eddie Kohler. Manageable fine-grained information flow. In Proceedings of the 3rd ACM EuroSys Conference, pages 301- 313, Glasgow, Scotland, April 2008.

Digital Library

[15]

Petros Efstathopoulos, Maxwell Krohn, Steve Van-DeBogart, Cliff Frey, David Ziegler, Eddie Kohler, David Mazières, M. Frans Kaashoek, and Robert Morris. Labels and event processes in the Asbestos operating system. In Proceedings of the 20th ACM Symposium on Operating Systems Principles (SOSP), pages 17-30, Brighton, United Kingdom, October 2005.

Digital Library

[16]

Sebastian Eggert. Security via Noninterference: Analyzing Information Flows. PhD thesis, Kiel University, July 2014.

[17]

Sebastian Eggert and Ron van der Meyden. Dynamic intransitive noninterference revisited. Formal Aspects of Computing, 29(6):1087-1120, June 2017.

[18]

Dawson R. Engler, M. Frans Kaashoek, and James W. O'Toole. Exokernel: An operating system architecture for application-level resource management. In Proceedings of the 15th ACM Symposium on Operating Systems Principles (SOSP), pages 251-266, Copper Mountain, CO, December 1995.

Digital Library

[19]

Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pages 287-305, Shanghai, China, October 2017.

Digital Library

[20]

Andrew Ferraiuolo, Rui Xu, Danfeng Zhang, Andrew C. Myers, and G. Edward Suh. Verification of a practical hardware security architecture through static information flow analysis. In Proceedings of the 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 555-568, Xi'an, China, April 2017.

Digital Library

[21]

Andrew Ferraiuolo, Mark Zhao, Andrew C. Myers, and G. Edward Suh. HyperFlow: A processor architecture for nonmalleable, timing-safe information flow security. In Proceedings of the 25th ACM Conference on Computer and Communications Security (CCS), Toronto, Canada, October 2018.

Digital Library

[22]

Qian Ge, Yuval Yarom, and Gernot Heiser. No security without time protection: We need a new hardware-software contract. In Proceedings of the 9th Asia-Pacific Workshop on Systems, Jeju Island, South Korea, August 2018.

Digital Library

[23]

Daniel B. Giffin, Amit Levy, Deian Stefan, David Terei, David Mazières, John C. Mitchell, and Alejandro Russo. Hails: Protecting data privacy in untrusted web applications. In Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Hollywood, CA, October 2012.

Digital Library

[24]

J. A. Goguen and J. Meseguer. Security policies and security models. In Proceedings of the 3rd IEEE Symposium on Security and Privacy, pages 11-20, Oakland, CA, April 1982.

[25]

John Graham-Cumming and J. W. Sanders. On the refinement of non-interference. In Proceedings of the Computer Security Foundations Workshop VI, pages 35-42, Franconia, NH, June 1991.

[26]

Ronghui Gu. Private communication, August 2018.

[27]

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 653-669, Savannah, GA, November 2016.

Digital Library

[28]

Zhenyu Guo, Xi Wang, Jian Tang, Xuezheng Liu, Zhilei Xu, Ming Wu, M. Frans Kaashoek, and Zheng Zhang. R2: An application-level kernel for record and replay. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 193-208, San Diego, CA, December 2008.

Digital Library

[29]

J. T. Haigh and W. D. Young. Extending the noninterference version of MLS for SAT. IEEE Transactions on Software Engineering, SE-13(2):141-150, February 1987.

Digital Library

[30]

William R. Harris, Somesh Jha, and Thomas Reps. DIFC programs by automatic instrumentation. In Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS), pages 284-296, Chicago, IL, October 2010.

Digital Library

[31]

William R. Harris, Somesh Jha, Thomas Reps, and Sanjit A. Seshia. Program synthesis for interactive-security systems. Formal Methods in System Design, 51(2):362-394, November 2017.

Digital Library

[32]

Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. Ironclad Apps: End-to-end security via automated full-system verification. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 165-181, Broomfield, CO, October 2014.

Digital Library

[33]

C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271-281, December 1972.

Digital Library

[34]

C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666-677, August 1978.

Digital Library

[35]

Suman Jana and Vitaly Shmatikov. Memento: Learning secrets from process footprints. In Proceedings of the 33rd IEEE Symposium on Security and Privacy, pages 143-157, San Francisco, CA, May 2012.

Digital Library

[36]

Dongseok Jang, Zachary Tatlock, and Sorin Lerner. Establishing browser security guarantees through formal shim verification. In Proceedings of the 21st USENIX Security Symposium, pages 113-128, Bellevue, WA, August 2012.

Digital Library

[37]

M. Frans Kaashoek, Dawson R. Engler, Gregory R. Ganger, Héctor M. Briceño, Russell Hunt, David Mazières, Thomas Pinckney, Robert Grimm, John Jannotti, and Kenneth Mackenzie. Application performance and flexibility on exokernel systems. In Proceedings of the 16th ACM Symposium on Operating Systems Principles (SOSP), pages 52-65, Saint-Malo, France, October 1997.

Digital Library

[38]

Richard A. Kemmerer. Shared resource matrix methodology: An approach to identifying storage and timing channels. ACM Transactions on Computer Systems, 1(3):256-277, August 1983.

Digital Library

[39]

Richard A. Kemmerer. A practical approach to identifying storage and timing channels: Twenty years later. In Proceedings of the 18th Annual Computer Security Applications Conference (ACSAC), pages 109-118, Las Vegas, NV, December 2002.

Digital Library

[40]

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Michael Norrish, Rafal Kolanski, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), pages 207-220, Big Sky, MT, October 2009.

Digital Library

[41]

Gerwin Klein, Thomas Sewell, and Simon Winwood. Refinement in the formal verification of the seL4 microkernel. In Design and Verification of Microprocessor Systems for High-Assurance Applications, pages 323-339. Springer, January 2010.

[42]

Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. Spectre attacks: Exploiting speculative execution. In Proceedings of the 40th IEEE Symposium on Security and Privacy, San Francisco, CA, May 2019.

[43]

Rafal Kolanski. Verification of Programs in Virtual Memory Using Separation Logic. PhD thesis, University of New South Wales, July 2011.

[44]

Maxwell Krohn and Eran Tromer. Noninterference for a practical DIFC-based operating system. In Proceedings of the 30th IEEE Symposium on Security and Privacy, pages 61-76, Oakland, CA, May 2009.

Digital Library

[45]

Maxwell Krohn, Alexander Yip, Micah Brodsky, Natan Cliffer, M. Frans Kaashoek, Eddie Kohler, and Robert Morris. Information flow control for standard OS abstractions. In Proceedings of the 21st ACM Symposium on Operating Systems Principles (SOSP), pages 321-334, Stevenson, WA, October 2007.

Digital Library

[46]

Leslie Lamport. Computation and state machines, April 2008.

[47]

Butler W. Lampson. A note on the confinement problem. Communications of the ACM, 16(10):613-615, October 1973.

Digital Library

[48]

Butler W. Lampson. Hints for computer system design. In Proceedings of the 9th ACM Symposium on Operating Systems Principles (SOSP), pages 33- 48, Bretton Woods, NH, October 1983.

Digital Library

[49]

Peng Li and Steve Zdancewic. Downgrading policies and relaxed noninterference. In Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL), pages 158-170, Long Beach, CA, January 2005.

Digital Library

[50]

Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. Meltdown: Reading kernel memory from user space. In Proceedings of the 27th USENIX Security Symposium, pages 973-990, Baltimore, MD, August 2018.

Digital Library

[51]

Lanyue Lu, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dusseau, and Shan Lu. A study of Linux file system evolution. ACM Transactions on Storage, 10 (1):31-44, January 2014.

Digital Library

[52]

Heiko Mantel. Preserving information flow properties under refinement. In Proceedings of the 22nd IEEE Symposium on Security and Privacy, pages 78-91, Oakland, CA, May 2001.

Digital Library

[53]

John McLean. Security models and information flow. In Proceedings of the 11th IEEE Symposium on Security and Privacy, pages 180-187, Oakland, CA, May 1990.

[54]

MITRE. CWE-209: Information exposure through an error message. https://cwe.mitre.org/data/definitions/209.html, January 2018.

[55]

Bodo Möller. Security of CBC ciphersuites in SSL/ TLS: Problems and countermeasures. https://www.openssl.org/~bodo/tls-cbc.txt, September 2014.

[56]

Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, and Gerwin Klein. Noninterference for operating system kernels. In Proceedings of the 2nd International Conference on Certified Programs and Proofs (CPP), pages 126-142, Kyoto, Japan, December 2012.

Digital Library

[57]

Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. seL4: from general purpose to a proof of information flow enforcement. In Proceedings of the 34th IEEE Symposium on Security and Privacy, pages 415-429, San Francisco, CA, May 2013.

Digital Library

[58]

Toby Murray, Robert Sison, and Kai Engelhardt. COVERN: A logic for compositional verification of information flow control. In Proceedings of the 3rd IEEE European Symposium on Security and Privacy, pages 16-30, London, United Kingdom, April 2018.

[59]

musl. https://www.musl-libc.org/, 2018.

[60]

Andrew Myers and Barbara Liskov. A decentralized model for information flow control. In Proceedings of the 16th ACM Symposium on Operating Systems Principles (SOSP), pages 129-147, Saint-Malo, France, October 1997.

Digital Library

[61]

Andrew C. Myers and Barbara Liskov. Protecting privacy using the decentralized label model. ACM Transactions on Computer Systems, 9(4):410-442, October 2000.

Digital Library

[62]

Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-button verification of an OS kernel. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pages 252-269, Shanghai, China, October 2017.

Digital Library

[63]

Nicolas Palix, Gaël Thomas, Suman Saha, Christophe Calvès, Julia L. Lawall, and Gilles Muller. Faults in Linux: Ten years later. In Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 305-318, Newport Beach, CA, March 2011.

Digital Library

[64]

Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock, and Sorin Lerner. Automating formal proofs for reactive systems. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 452-462, Edinburgh, United Kingdom, June 2014.

Digital Library

[65]

Indrajit Roy, Donald E. Porter, Michael D. Bond, Kathryn S. McKinley, and Emmett Witchel. Laminar: Practical fine-grained decentralized information flow control. In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Dublin, Ireland, June 2009.

Digital Library

[66]

John Rushby. Design and verification of secure systems. In Proceedings of the 8th ACM Symposium on Operating Systems Principles (SOSP), pages 12-21, Pacific Grove, CA, December 1981.

Digital Library

[67]

John Rushby. Noninterference, transitivity, and channel-control security policies. Technical Report CSL-92-02, SRI International, December 1992.

[68]

Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul Karger Vernon Austel, and David Toll. Verification of a formal security model for multiapplicative smart cards. In Proceedings of the 6th European Symposium on Research in Computer Security, pages 17-36, Toulouse, France, October 2000.

Digital Library

[69]

Jonathan S. Shapiro, Jonathan M. Smith, and David J. Farber. EROS: a fast capability system. In Proceedings of the 17th ACM Symposium on Operating Systems Principles (SOSP), pages 170-185, Kiawah Island, SC, December 1999.

Digital Library

[70]

Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-button verification of file systems via crash refinement. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 1-16, Savannah, GA, November 2016.

Digital Library

[71]

Deian Stefan, Alejandro Russo, Pablo Buiras, Amit Levy, John C. Mitchell, and David Mazières. Addressing covert termination and timing channels in concurrent information flow systems. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 201-214, Copenhagen, Denmark, September 2012.

Digital Library

[72]

Zachary Tatlock and Sorin Lerner. Bringing extensibility to verified compilers. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 111-121, Toronto, Canada, June 2010.

Digital Library

[73]

Tachio Terauchi and Alex Aiken. Secure information flow as a safety problem. In Proceedings of the 12th International Static Analysis Symposium (SAS), pages 352-367, London, United Kingdom, September 2005.

Digital Library

[74]

The Coq Development Team. The Coq Proof Assistant, version 8.8.0, April 2018.

[75]

Ta-chung Tsai, Alejandro Russo, and John Hughes. Alibrary for secure multi-threaded information flow in Haskell. In Proceedings of the 20th IEEE Computer Security Foundations Symposium, pages 187- 202, Venice, Italy, July 2007.

Digital Library

[76]

Ron van der Meyden. Architectural refinement and notions of intransitive noninterference. Formal Aspects of Computing, 24(4-6):769-792, July 2012.

[77]

David von Oheimb. Information flow control revisited: Noninfluence = noninterference + nonleakage. In Proceedings of the 9th European Symposium on Research in Computer Security, pages 225-243, Sophia Antipolis, France, September 2004.

[78]

Xi Wang, Nickolai Zeldovich, M. Frans Kaashoek, and Armando Solar-Lezama. Towards optimization-safe systems: Analyzing the impact of undefined behavior. In Proceedings of the 24th ACM Symposium on Operating Systems Principles (SOSP), pages 260-275, Farmington, PA, November 2013.

Digital Library

[79]

Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock. SpaceSearch: A library for building and verifying solver-aided tools. In Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP), Oxford, United Kingdom, September 2017.

Digital Library

[80]

Steve Zdancewic and Andrew C. Myers. Robust declassification. In Proceedings of the 14th IEEE workshop on Computer Security Foundations, Cape Breton, Canada, June 2001.

Digital Library

[81]

Nickolai Zeldovich. Private communication, April 2018.

[82]

Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazières. Making information flow explicit in HiStar. In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 263-278, Seattle, WA, November 2006.

Digital Library

[83]

Nickolai Zeldovich, Silas Boyd-Wickizer, and David Mazières. Securing distributed systems with information flow control. In Proceedings of the 5th USENIX Symposium on Networked Systems Design and Implementation (NSDI), pages 293-308, San Francisco, CA, April 2008.

Digital Library

[84]

Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazières. Making information flow explicit in HiStar. Communications of the ACM, 54(11):93-101, November 2011.

Digital Library

[85]

Kehuan Zhang and XiaoFeng Wang. Peeping Tom in the neighborhood: Keystroke eavesdropping on multi-user systems. In Proceedings of the 18th USENIX Security Symposium, pages 17-32, Montreal, Canada, August 2009.

Digital Library

[86]

Yongwang Zhao, David Sanán, Fuyuan Zhang, and Yang Liu. Reasoning about information flow security of separation kernels with channel-based communication. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 791-810, Eindhoven, The Netherlands, April 2016.

Digital Library

Cited By

Zhuo DZhang KLi ZZhuang SWang SChen AStoica I(2022)Rearchitecting in-memory object stores for low latencyProceedings of the VLDB Endowment10.14778/3494124.349413815:3(555-568)Online publication date: 4-Feb-2022
https://dl.acm.org/doi/10.14778/3494124.3494138
Zhang KZhuo DAkella AKrishnamurthy AWang XBhagwan RPorter G(2020)Automated verification of customizable middlebox properties with gravelProceedings of the 17th Usenix Conference on Networked Systems Design and Implementation10.5555/3388242.3388258(221-240)Online publication date: 25-Feb-2020
https://dl.acm.org/doi/10.5555/3388242.3388258
Nelson LBornholt JKrishnamurthy ATorlak EWang X(2020)Noninterference specifications for secure systemsACM SIGOPS Operating Systems Review10.1145/3421473.342147854:1(31-39)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421478
Show More Cited By

Nickel: a framework for design and verification of information flow control systems

Recommendations

Morphology control of nickel oxide nanowires

Graphical abstractDisplay Omitted Highlights Nickel oxide (NiO) nanowires are synthesized by the hydroxylation and dehydration of nickel. The morphology of NiO nanowires can be controlled by controlling parameters such as annealing temperature and ...
Synthesis and characterization of nanostructured nickel diselenide nise₂ from the decomposition of nickel acetate, (CH₃CO₂)₂Ni
Special issue on Chalcogenide Nanomaterials: Synthesis Characterization and Applications

Solution processed NiSe₂ nanorods were synthesized by a modified colloidal synthesis technique, by chemical reaction of TOPSe and nickel acetate at 150°C. The rods exist as an oleic acid ligand stabilized solution, with oleic acid acting as a capping ...
Electrodeposition and Characterisation of Nickel, Germanium and Tin Thin Films

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

OSDI'18: Proceedings of the 13th USENIX conference on Operating Systems Design and Implementation

October 2018

815 pages

ISBN:9781931971478

Program Chairs:
Andrea Arpaci-Dusseau
University of Wisconsin-Madison
,
Geoff Voelker
University of California, San Diego

Sponsors

NetApp
Google Inc.
NSF
Microsoft: Microsoft
Facebook: Facebook

In-Cooperation

SIGOPS: ACM Special Interest Group on Operating Systems

Publisher

USENIX Association

United States

Publication History

Published: 08 October 2018

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhuo DZhang KLi ZZhuang SWang SChen AStoica I(2022)Rearchitecting in-memory object stores for low latencyProceedings of the VLDB Endowment10.14778/3494124.349413815:3(555-568)Online publication date: 4-Feb-2022
https://dl.acm.org/doi/10.14778/3494124.3494138
Zhang KZhuo DAkella AKrishnamurthy AWang XBhagwan RPorter G(2020)Automated verification of customizable middlebox properties with gravelProceedings of the 17th Usenix Conference on Networked Systems Design and Implementation10.5555/3388242.3388258(221-240)Online publication date: 25-Feb-2020
https://dl.acm.org/doi/10.5555/3388242.3388258
Nelson LBornholt JKrishnamurthy ATorlak EWang X(2020)Noninterference specifications for secure systemsACM SIGOPS Operating Systems Review10.1145/3421473.342147854:1(31-39)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421478
Erbsen APhilipoom JGross JSloan RChlipala A(2020)Simple High-Level Code For Cryptographic ArithmeticACM SIGOPS Operating Systems Review10.1145/3421473.342147754:1(23-30)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421477
Vasudevan AManiatis PMartins R(2020)überSparkACM SIGOPS Operating Systems Review10.1145/3421473.342147654:1(8-22)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421476

View Options

View options

Media

Figures

Other

Tables

View Table of Contents