-
Notifications
You must be signed in to change notification settings - Fork 6
/
cheri.bib
16839 lines (14807 loc) · 597 KB
/
cheri.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
@techreport{CHERI-FM15,
author = {Peter G. Neumann and Robert N. M. Watson and Nirav Dave and Alexandre Joannou and Matthew Naylor and Michael Roe and Anthony Fox and Jonathan Woodruff},
title = {{CHERI Formal Methods, interim version 3.0}},
year = {2015},
source = {},
institution = {SRI International and the University of Cambridge},
address = {},
}
@article{karger:performance,
author = {Karger, Paul A.},
title = {Using registers to optimize cross-domain call performance},
journal = {SIGARCH Computer Architecture News},
volume = {17},
number = {2},
year = {1989},
issn = {0163-5964},
pages = {194--204},
doi = {10.1145/68182.68201},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{demoura-etal07:VSTTE,
AUTHOR = {Leonardo de Moura and Sam Owre and Harald Rue{\ss} and
John Rushby and Natarajan Shankar},
TITLE = {Integrating Verification Components},
CROSSREF = {VSTTE07}
}
@proceedings{VSTTE07,
TITLE = {Verified Software:
Theories, Tools, and Experiments},
BOOKTITLE = {Verified Software:
Theories, Tools, and Experiments},
EDITOR = {Bertrand Meyer and Jim Woodcock},
NUMBER = 4171,
SERIES = {LNCS},
YEAR = 2008
}
@comment{ PUBLISHER = {Springer Verlag}, }
@techreport{andrews:partitions,
author = {Andrews, Gregory R.},
title = {Partitions and Principles for Secure Operating Systems},
year = {1975},
source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Acornellcs%3ACORNELLCS%3ATR75-228},
institution = {Cornell University},
address = {Ithaca, NY, USA},
}
@article{wulf:hydra,
author = {Wulf, W. and Cohen, E. and Corwin, W. and Jones, A. and Levin, R. and Pierson, C. and Pollack, F.},
title = {{HYDRA: the kernel of a multiprocessor operating system}},
journal = {Communications of the ACM},
volume = {17},
number = {6},
year = {1974},
issn = {0001-0782},
pages = {337--345},
doi = {10.1145/355616.364017},
publisher = {ACM},
address = {New York, NY, USA},
}
@article{walker:uclasecureunix,
author = {Walker, Bruce J. and Kemmerer, Richard A. and Popek, Gerald J.},
title = {{Specification and verification of the UCLA Unix security kernel}},
journal = {Communications of the ACM},
volume = {23},
number = {2},
year = {1980},
issn = {0001-0782},
pages = {118--131},
doi = {10.1145/358818.358825},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{schroeder:multicssecuritykernel,
author = {Schroeder, Michael D.},
title = {{Engineering a security kernel for Multics}},
booktitle = {SOSP '75: Proceedings of the Fifth ACM Symposium on Operating Systems Principles},
year = {1975},
pages = {25--32},
location = {Austin, Texas, United States},
doi = {10.1145/800213.806518},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{walker:adventtrusted,
author = {Walker, Stephen T.},
title = {The advent of trusted computer operating systems},
booktitle = {AFIPS '80: Proceedings of the May 19-22, 1980, national computer conference},
year = {1980},
pages = {655--665},
location = {Anaheim, California},
doi = {10.1145/1500518.1500626},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{sebes:dtmach,
author = {E. J. Sebes},
booktitle = {{Proceedings of the USENIX Mach Symposium}},
title = {{Overview of the architecture of Distributed Trusted Mach}},
pages = {20--22},
month = nov,
year = {1991},
pmid = {286502042582210013related:3VWJ-xbc-QMJ},
publisher = {USENIX Association},
}
@InProceedings{spencer:flask,
author = "Ray Spencer and Stephen Smalley and Peter Loscocco and
Mike Hibler and David Andersen and Jay Lepreau",
title = "The {Flask} Security Architecture: System Support for
Diverse Security Policies",
annote = "Separate policy and mechanisms derived from DTOS and
somewhat consistant with GFAC. Not so suitable:
Capability systems (difficulty to control propagation)
and interception systesm (e.g., L4 Clan/Chief, problem
of exposure of all abstractions). Fluke (\& flask)
homepage:
\url{http://www.cs.utah.edu/flux/fluke/html/flask.html}",
pages = "123--139",
booktitle = "{Proceedings of the 8th {USENIX} Security Symposium}",
year = "1999",
publisher = {USENIX Association},
month = aug,
address = "Washington, D.C., USA",
}
@inproceedings{wang:gazelle,
author = {Wang, Helen J. and Grier, Chris and Moshchuk, Alexander and King, Samuel T. and Choudhury, Piali and Venter, Herman},
title = {{The multi-principal OS construction of the Gazelle web browser}},
booktitle = {Proceedings of the 18th USENIX Security Symposium},
year = {2009},
pages = {417--432},
location = {Montreal, Canada},
publisher = {USENIX Association},
address = {Berkeley, CA, USA},
}
@inproceedings{remy:ocaml,
author = {R\'{e}my, Didier and Vouillon, J\'{e}r\^{o}me},
title = {{Objective ML: a simple object-oriented extension of ML}},
booktitle = {{POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}},
year = {1997},
isbn = {0-89791-853-3},
pages = {40--53},
location = {Paris, France},
doi = {10.1145/263699.263707},
publisher = {ACM},
address = {New York, NY, USA},
}
@book{mckusick:freebsd,
author = {McKusick, Marshall Kirk and Neville-Neil, George V. and Watson,
Robert N. M.},
title = {{The Design and Implementation of the FreeBSD Operating System,
Second Edition}},
year = {2014},
publisher = {Pearson Education},
}
@misc{ruby,
title = {{Ruby Programming Language}},
howpublished = {\url{http://www.ruby-lang.org/}},
author = {{Ruby Users Group}},
year = 2010,
month = oct,
}
@inproceedings{trevor:cyclone,
author = {Jim, Trevor and Morrisett, J. Greg and Grossman, Dan and Hicks, Michael W. and Cheney, James and Wang, Yanling},
title = {Cyclone: A Safe Dialect of~{C}},
booktitle = {{ATEC '02: Proceedings of the USENIX Annual Technical Conference}},
year = {2002},
isbn = {1-880446-00-6},
pages = {275--288},
publisher = {USENIX Association},
address = {Berkeley, CA, USA},
}
@inproceedings{cantrill:dtrace,
author = {Cantrill, Bryan M. and Shapiro, Michael W. and Leventhal, Adam H.},
title = {Dynamic instrumentation of production systems},
booktitle = {ATEC '04: Proceedings of the USENIX Annual Technical Conference},
year = {2004},
location = {Boston, MA},
publisher = {{USENIX Association}},
address = {Berkeley, CA, USA},
}
@inproceedings{necula:pcc,
author = {Necula, George C. and Lee, Peter},
title = {Safe kernel extensions without run-time checking},
booktitle = {OSDI '96: Proceedings of the Second USENIX symposium on Operating Systems Design and Implementation},
year = {1996},
isbn = {1-880446-82-0},
pages = {229--243},
location = {Seattle, Washington, United States},
doi = {10.1145/238721.238781},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{yee:nativeclient,
author = {Yee, Bennet and Sehr, David and Dardyk, Gregory and Chen, J. Bradley and Muth, Robert and Ormandy, Tavis and Okasaka, Shiki and Narula, Neha and Fullagar, Nicholas},
title = {Native Client: A Sandbox for Portable, Untrusted x86 Native Code},
booktitle = {SP '09: Proceedings of the 2009 30th IEEE Symposium on Security and Privacy},
year = {2009},
isbn = {978-0-7695-3633-0},
pages = {79--93},
doi = {10.1109/SP.2009.25},
publisher = {IEEE Computer Society},
address = {Washington, DC, USA},
}
@inproceedings{mccanne:bpf,
author = {McCanne, Steven and Jacobson, Van},
title = {{The BSD packet filter: a new architecture for user-level packet capture}},
booktitle = {{USENIX'93: Proceedings of the USENIX Winter 1993 Conference}},
year = {1993},
location = {San Diego, California},
publisher = {USENIX Association},
address = {Berkeley, CA, USA},
}
@inproceedings{bershad:spin,
author = {Bershad, B. N. and Savage, S. and Pardyak, P. and Sirer, E. G. and Fiuczynski, M. E. and Becker, D. and Chambers, C. and Eggers, S.},
title = {{Extensibility safety and performance in the SPIN operating system}},
booktitle = {{SOSP '95: Proceedings of the Fifteenth ACM Symposium on Operating Systems Principles}},
year = {1995},
isbn = {0-89791-715-4},
pages = {267--283},
location = {Copper Mountain, Colorado, United States},
doi = {10.1145/224056.224077},
publisher = {ACM},
address = {New York, NY, USA},
}
@article{myers:difc,
author = {Myers, Andrew C. and Liskov, Barbara},
title = {A decentralized model for information flow control},
journal = {SIGOPS Oper. Syst. Rev.},
volume = {31},
issue = {5},
month = oct,
year = {1997},
issn = {0163-5980},
pages = {129--142},
numpages = {14},
doi = {10.1145/269005.266669},
acmid = {266669},
publisher = {ACM},
address = {New York, NY, USA},
}
@article{efstathopoulos:asbestos,
author = {Efstathopoulos, Petros and Krohn, Maxwell and VanDeBogart, Steve and Frey, Cliff and Ziegler, David and Kohler, Eddie and Mazi\`{e}res, David and Kaashoek, Frans and Morris, Robert},
title = {Labels and event processes in the asbestos operating system},
journal = {SIGOPS Oper. Syst. Rev.},
volume = {39},
issue = {5},
month = oct,
year = {2005},
issn = {0163-5980},
pages = {17--30},
numpages = {14},
doi = {10.1145/1095809.1095813},
acmid = {1095813},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {event processes, information flow, labels, mandatory access control, secure web servers},
}
@inproceedings{zeldovich:histar,
author = {Zeldovich, Nickolai and Boyd-Wickizer, Silas and Kohler, Eddie and Mazi\`{e}res, David},
title = {Making information flow explicit in {HiStar}},
booktitle = {Proceedings of the 7th symposium on Operating systems design and implementation},
series = {OSDI '06},
year = {2006},
isbn = {1-931971-47-1},
location = {Seattle, Washington},
pages = {263--278},
numpages = {16},
url = {http://portal.acm.org/citation.cfm?id=1298455.1298481},
acmid = {1298481},
publisher = {USENIX Association},
address = {Berkeley, CA, USA},
}
@inproceedings{boebert:inabilitystar,
title = {On the Inability of an Unmodified Capability Machine to Enforce the *-Property},
booktitle = {Proc. 7th {{DoD}}/{{NBS Computer Security Conference}}},
author = {Boebert, William Earl},
date = {1984-09},
pages = {291--293},
url = {https://csrc.nist.gov/CSRC/media/Publications/conference-paper/1984/09/24/7th-dod-nbs-computer-security-conference/documents/1984-7th-conference-proceedings.pdf},
eventtitle = {{{DoD}}/{{NBS Computer Security Conference}}}
}
@article{hardy:keykos,
author = {Hardy, Norman},
title = {{KeyKOS architecture}},
journal = {SIGOPS Operating Systems Review},
volume = {19},
number = {4},
year = {1985},
issn = {0163-5980},
pages = {8--25},
doi = {10.1145/858336.858337},
publisher = {ACM},
address = {New York, NY, USA},
note = {Also available at \url{http://cap-lore.com/CapTheory/upenn/OSRpaper.html}}
}
@inproceedings{shapiro:eros,
author = {Jonathan Shapiro and Jonathan Smith and David Farber},
booktitle = {{SOSP '99: Proceedings of the seventeenth ACM Symposium on Operating Systems Principles}},
title = {{EROS: a fast capability system}},
abstract = {EROS is a capability-based operating system for commodity processors which uses a single level storage model. The single level store's persistence is transparent to applications. The performance consequences of support for transparent persistence and ...},
year = {1999},
month = dec,
pmid = {319151.319163},
url = {http://portal.acm.org/citation.cfm?id=319151.319163},
howpublished = {\url{http://portal.acm.org/citation.cfm?id=319151.319163}},
}
@misc{shapiro:coyotosspec,
author={Jonathan S. Shapiro and Jonathan W. Adams},
title={Coyotos Microkernel Specification},
subtitle={Version 0.6+},
date={2007-09-10},
url={https://web.archive.org/web/20160904092954/http://www.coyotos.org:80/docs/ukernel/spec.html}
}
@inproceedings{mettler:joee,
author = {Mettler, Adrian and Wagner, David},
title = {{Class properties for security review in an object-capability subset of Java}},
booktitle = {PLAS '10: Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security},
year = {2010},
isbn = {978-1-60558-827-8},
pages = {1--7},
location = {Toronto, Canada},
doi = {10.1145/1814217.1814224},
publisher = {ACM},
address = {New York, NY, USA},
}
@misc{miller:elang,
author = {Mark S. Miller},
title = {The E Language},
note = "\url{http://www.erights.org/}",
}
@misc{miller:caja,
author = {Mark S. Miller and Mike Samuel and Ben Laurie and Ihab Awad and Mike Stay},
title = {Caja: Safe active content in Sanitized JavaScript},
month = may,
year = {2008},
institution = {Google},
url = {http://google-caja.googlecode.com/files/caja-spec-2008-06-07.pdf},
note = "\url{http://google-caja.googlecode.com/files/caja-spec-2008-06-07.pdf}",
}
@article{miller:capmyths,
title = {Capability {Myths} {Demolished}},
abstract = {We address three common misconceptions about capability-based systems: the Equivalence Myth (access control list systems and capability systems are formally equivalent), the Confinement Myth (capability systems cannot enforce confinement), and the Irrevocability Myth (capability-based access cannot be revoked). The Equivalence Myth obscures the benefits of capabilities as compared to access control lists, while the Confinement Myth and the Irrevocability Myth lead people to see problems with capabilities that do not actually exist.},
language = {en},
author = {Miller, Mark S and Yee, Ka-Ping and Shapiro, Jonathan},
pages = {15},
url = {http://srl.cs.jhu.edu/pubs/SRL2003-02.pdf}
}
@article{miller:paradigmregained,
address = {Berlin, Heidelberg},
title = {Paradigm {Regained}: {Abstraction} {Mechanisms} for {Access} {Control}},
isbn = {978-3-540-40965-6},
abstract = {Access control systems must be evaluated in part on how well they enable one to distribute the access rights needed for cooperation, while simultaneously limiting the propagation of rights which would create vulnerabilities. Analysis to date implicitly assumes access is controlled only by manipulating a system's protection state – the arrangement of the access graph. Because of the limitations of this analysis, capability systems have been ”proven” unable to enforce some basic policies: revocation, confinement, and the *-properties (explained in the text).},
booktitle = {Advances in {Computing} {Science} – {ASIAN} 2003. {Progamming} {Languages} and {Distributed} {Computation} {Programming} {Languages} and {Distributed} {Computation}},
publisher = {Springer Berlin Heidelberg},
author = {Miller, Mark S. and Shapiro, Jonathan S.},
editor = {Saraswat, Vijay A.},
year = {2003},
pages = {224--242},
url = {http://www.erights.org/talks/asian03/}
}
@phdthesis{miller:robustcomposition,
author = {Miller, Mark Samuel},
title = {Robust composition: towards a unified approach to access control and concurrency control},
year = {2006},
order_no = {AAI3245526},
school = {Johns Hopkins University},
address = {Baltimore, MD, USA},
}
@book{gosling:javalanguage,
author = {Gosling, James and Joy, Bill and Steele, Guy L.},
title = {The Java Language Specification},
year = {1996},
isbn = {0201634511},
publisher = {Addison-Wesley Longman Publishing Co., Inc.},
address = {Boston, MA, USA},
}
@inproceedings{lipner:securitykernels,
author = {Lipner, Steven B. and Wulf, William A. and Schell, Roger R. and Popek, Gerald J. and Neumann, Peter G. and Weissman, Clark and Linden, Theodore A.},
title = {Security kernels},
booktitle = {AFIPS '74: Proceedings of the May 6-10, 1974, National Computer Conference and Exposition},
year = {1974},
pages = {973--980},
location = {Chicago, Illinois},
doi = {10.1145/1500175.1500361},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{ackerman:multiprocessing,
author = {Ackerman, William B. and Plummer, William W.},
title = {An implementation of a multiprocessing computer system},
booktitle = {SOSP '67: Proceedings of the First ACM Symposium on Operating System Principles},
year = {1967},
pages = {5.1--5.10},
doi = {10.1145/800001.811666},
publisher = {ACM},
address = {New York, NY, USA},
}
@article{ritchie:unix,
author = {Ritchie, Dennis M. and Thompson, Ken},
title = {{The UNIX time-sharing system}},
journal = {Communications of the ACM},
volume = {17},
number = {7},
year = {1974},
issn = {0001-0782},
pages = {365--375},
doi = {10.1145/361011.361061},
publisher = {ACM},
address = {New York, NY, USA},
}
@article{denning:faulttolerance,
author = {Denning, Peter J.},
title = {Fault Tolerant Operating Systems},
journal = {ACM Computing Surveys},
volume = {8},
number = {4},
year = {1976},
issn = {0360-0300},
pages = {359--389},
doi = {10.1145/356678.356680},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{patterson:risc,
author = {Patterson, David A. and Sequin, Carlo H.},
title = {{RISC I: A Reduced Instruction Set VLSI Computer}},
booktitle = {ISCA '81: Proceedings of the 8th Annual Symposium on Computer Architecture},
year = {1981},
pages = {443--457},
location = {Minneapolis, Minnesota, United States},
publisher = {IEEE Computer Society Press},
address = {Los Alamitos, CA, USA},
}
@inproceedings{corbato:multics,
author = {Corbat\'{o}, F. J. and Vyssotsky, V. A.},
title = {{Introduction and overview of the Multics system}},
booktitle = {AFIPS '65 (Fall, part I): Proceedings of the November 30--December 1, 1965, Fall Joint Computer Conference, part I},
year = {1965},
pages = {185--196},
location = {Las Vegas, Nevada},
doi = {10.1145/1463891.1463912},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{corbato:timesharing,
author = {Corbat\'{o}, Fernando J. and Merwin-Daggett, Marjorie and Daley, Robert C.},
title = {An experimental time-sharing system},
booktitle = {AIEE-IRE '62 (Spring): Proceedings of the May 1--3, 1962, Spring Joint Computer Conference},
year = {1962},
pages = {335--344},
location = {San Francisco, California},
doi = {10.1145/1460833.1460871},
publisher = {ACM},
address = {New York, NY, USA},
}
@article{dennis:semantics,
author = {Dennis, Jack B. and Van Horn, Earl C.},
title = {Programming semantics for multiprogrammed computations},
journal = {Communications of the ACM},
volume = {9},
number = {3},
year = {1966},
issn = {0001-0782},
pages = {143--155},
doi = {10.1145/365230.365252},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{reis:chromium,
author = {Reis, Charles and Gribble, Steven D.},
title = {Isolating web programs in modern browser architectures},
booktitle = {EuroSys '09: Proceedings of the 4th ACM European Conference on Computer Systems},
year = {2009},
isbn = {978-1-60558-482-9},
pages = {219--232},
location = {Nuremberg, Germany},
doi = {10.1145/1519065.1519090},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{provos:preventingprivesc,
author = {Neils Provos and Markus Friedl and Peter Honeyman},
booktitle = {{Proceedings of the 12th USENIX Security Symposium}},
title = {{Preventing Privilege Escalation}},
year = {2003},
publisher = {USENIX Association},
}
@inproceedings{bittau:wedge,
author = {Andrea Bittau and Petr Marchenko and Mark Handley and Brad Karp},
booktitle = {{Proceedings of the 5th USENIX Symposium on Networked Systems Design and Implementation}},
title = {{Wedge: Splitting Applications into Reduced-Privilege Compartments}},
school = {University College London},
pages = {309--322},year = {2008},
url = {http://www.cs.ucl.ac.uk/staff/m.handley/papers/wedge.pdf},
howpublished = {\url{http://www.cs.ucl.ac.uk/staff/m.handley/papers/wedge.pdf}},
publisher = {USENIX Association},
}
@techreport{accetta:mach,
author = "M. Accetta and R. Baron and D. Golub and R. Rashid and A.
Tevanian and M. Young",
institution = "{Computer Science Department, Carnegie Mellon
University}",
title = "{Mach: A New Kernel Foundation for UNIX Development}",
year = "1986",
month = aug,
}
@InProceedings{liedtke:l4,
author = {Jochen Liedtke},
title = {On Microkernel Construction},
booktitle = {SOSP'95: Proceedings of the
15th ACM Symposium on Operating System Principles},
address = {Copper Mountain Resort, CO},
month = dec,
year = 1995,
url = {http://l4ka.org/publications/}
}
@book{levy:capabilities,
author = {Levy, Henry M.},
title = {Capability-Based Computer Systems},
year = {1984},
isbn = {0932376223},
publisher = {Butterworth-Heinemann},
address = {Newton, MA, USA},
}
@inproceedings{yee:nacl,
author = {Yee, Bennet and Sehr, David and Dardyk, Gregory and Chen, J. Bradley and Muth, Robert and Ormandy, Tavis and Okasaka, Shiki and Narula, Neha and Fullagar, Nicholas},
title = {Native Client: A Sandbox for Portable, Untrusted x86 Native Code},
booktitle = {Proceedings of the 2009 30th IEEE Symposium on Security and Privacy},
year = {2009},
isbn = {978-0-7695-3633-0},
pages = {79--93},
numpages = {15},
url = {http://portal.acm.org/citation.cfm?id=1607723.1608126},
doi = {10.1109/SP.2009.25},
acmid = {1608126},
publisher = {IEEE Computer Society},
address = {Washington, DC, USA},
keywords = {Security, World Wide Web},
}
@inproceedings{wahbe:sfi,
author = {Wahbe, Robert and Lucco, Steven and Anderson, Thomas E. and Graham, S
usan L.},
title = {Efficient software-based fault isolation},
booktitle = {SOSP '93: Proceedings of the Fourteenth ACM Symposium on Operating
Systems Principles},
year = {1993},
isbn = {0-89791-632-8},
pages = {203--216},
location = {Asheville, North Carolina, United States}, doi = {10.1145/168619.168635},
publisher = {ACM},
address = {New York, NY, USA},
}
@article{richards:bluespecreasoning,
author = {Richards, Dominic and Lester, David},
affiliation = {School of Computer Science, The University of Manchester, Manchester, UK},
title = {{A monadic approach to automated reasoning for Bluespec SystemVerilog}},
journal = {Innovations in Systems and Software Engineering},
publisher = {Springer London},
issn = {1614-5046},
keyword = {Computer Science},
pages = {1-11},
note = {10.1007/s11334-011-0149-0},
year = {2011}
}
@InProceedings{NeumannWatson10LAW,
Author={Peter G. Neumann and Robert N.~M. Watson},
Title={Capabilities Revisited: A Holistic Approach to
Bottom-to-Top Assurance of Trustworthy Systems},
BookTitle={Fourth Layered Assurance Workshop},
Organization={U.S. Air Force Cryptographic Modernization Office and AFRL},
Address={Austin, Texas},
Year={2010}, Month=dec, pages={}, Note =
{http://www.csl.sri.com/neumann/law10.pdf}}
@InProceedings{Watson07,
Author={Robert N.~M. Watson},
Title={Exploiting Concurrency Vulnerabilities in System Call Wrappers},
BookTitle={WOOT Workshop},
Organization={USENIX Security}, Address={Gaithersburg, Maryland},
Year={2007}, Month={}, pages={}, Note = {
http://www.watson.org/~robert/2007woot/20070806-woot-concurrency.pdf}}
@PhdThesis{Drimer10,
author = {Saar Drimer},
title = {Security for Volatile FPGAs},
school = {University of Cambridge},
year = {2010} }
@inproceedings{Cadar:2008:KUA:1855741.1855756,
author = {Cadar, Cristian and Dunbar, Daniel and Engler, Dawson},
title = {{KLEE}: unassisted and automatic generation of high-coverage tests for complex systems programs},
booktitle = {Proceedings of the 8th USENIX conference on operating systems design and implementation},
series = {OSDI'08},
year = {2008},
location = {San Diego, California},
pages = {209--224},
numpages = {16},
url = {http://portal.acm.org/citation.cfm?id=1855741.1855756},
acmid = {1855756},
publisher = {USENIX Association},
address = {Berkeley, CA, USA},
}
@inproceedings{Yanagisawa:2006:DAS:1173706.1173717,
author = {Yanagisawa, Yoshisato and Kourai, Kenichi and Chiba, Shigeru},
title = {A dynamic aspect-oriented system for {OS} kernels},
booktitle = {Proceedings of the 5th international conference on Generative programming and component engineering},
series = {GPCE '06},
year = {2006},
isbn = {1-59593-237-2},
location = {Portland, Oregon, USA},
pages = {69--78},
numpages = {10},
doi = {10.1145/1173706.1173717},
acmid = {1173717},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Linux, aspect-oriented programming, dynamic AOP, operating system, profiling and debugging},
}
@article{Nethercote:2007:VFH:1273442.1250746,
author = {Nethercote, Nicholas and Seward, Julian},
title = {Valgrind: a framework for heavyweight dynamic binary instrumentation},
journal = {SIGPLAN Not.},
volume = {42},
issue = {6},
month = jun,
year = {2007},
issn = {0362-1340},
pages = {89--100},
numpages = {12},
doi = {10.1145/1273442.1250746},
acmid = {1250746},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Memcheck, Valgrind, dynamic binary analysis, dynamic binary instrumentation, shadow values},
}
@INPROCEEDINGS{Weimer05miningtemporal,
author = {Westley Weimer and George C. Necula},
title = {Mining Temporal Specifications for Error Detection},
booktitle = {In TACAS},
year = {2005},
pages = {461--476}
}
@inproceedings{muvi:sosp2007,
author = "Shan Lu and Soyeon Park and Chongfeng Hu and Xiao Ma and Weihang Jiang and Zhenmin Li and Raluca A. Popa and Yuanyuan Zhou",
title = "MUVI: Automatically Inferring Multi-Variable Access Correlations and Detecting Related Semantic and Concurrency Bugs",
booktitle = "Proceedings of the 21st ACM Symposium on Operating Systems Principles (SOSP07)",
month = oct,
year = "2007",
}
@misc{rfc4252,
author="T. Ylonen and C. Lonvick",
title="{The Secure Shell (SSH) Authentication Protocol}",
series="Request for Comments",
number="4252",
howpublished="RFC 4252 (Proposed Standard)",
publisher="IETF",
organisation="Internet Engineering Task Force",
year=2006,
month=jan,
url="http://www.ietf.org/rfc/rfc4252.txt",
}
@article{Bishop:2005:RSC:1090191.1080123,
author = {Bishop, Steve and Fairbairn, Matthew and Norrish, Michael and Sewell, Peter and Smith, Michael and Wansbrough, Keith},
title = {Rigorous specification and conformance testing techniques for network protocols, as applied to {TCP}, {UDP}, and sockets},
journal = {SIGCOMM Comput. Commun. Rev.},
issue_date = {October 2005},
volume = {35},
issue = {4},
month = aug,
year = {2005},
issn = {0146-4833},
pages = {265--276},
numpages = {12},
doi = {10.1145/1090191.1080123},
acmid = {1080123},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {API, HOL, TCP/IP, conformance testing, higher-order logic, network protocols, operational semantics, sockets, specification},
}
@inproceedings{Madhavapeddy:2009:CSM:1695271.1695302,
author = {Madhavapeddy, Anil},
title = {Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language},
booktitle = {Proceedings of the 11th International Conference on Formal Engineering Methods: Formal Methods and Software Engineering},
series = {ICFEM '09},
year = {2009},
isbn = {978-3-642-10372-8},
location = {Rio de Janeiro, Brazil},
pages = {446--465},
numpages = {20},
doi = {10.1007/978-3-642-10373-5_23},
acmid = {1695302},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
}
@inproceedings{Baldwin:2002:LMF:1250894.1250898,
author = {Baldwin, John H.},
title = {Locking in the multithreaded {FreeBSD} kernel},
booktitle = {Proceedings of the BSD Conference 2002},
series = {BSDC'02},
year = {2002},
location = {San Francisco, California},
pages = {4--4},
numpages = {1},
url = {http://portal.acm.org/citation.cfm?id=1250894.1250898},
acmid = {1250898},
publisher = {USENIX Association},
address = {Berkeley, CA, USA},
}
@inproceedings{LA04,
title = {{{LLVM}}: {{A Compilation Framework}} for {{Lifelong Program Analysis}} \& {{Transformation}}},
shorttitle = {{{LLVM}}},
booktitle = {Proceedings of the {{International Symposium}} on {{Code Generation}} and {{Optimization}}: {{Feedback}}-Directed and {{Runtime Optimization}}},
author = {Lattner, Chris and Adve, Vikram},
date = {2004-03},
pages = {75--86},
publisher = {{IEEE Computer Society}},
location = {{Washington, DC, USA}},
doi = {10.1109/CGO.2004.1281665},
url = {http://dl.acm.org/citation.cfm?id=977395.977673},
abstract = {This paper describes LLVM (Low Level Virtual Machine),a compiler framework designed to support transparent, lifelongprogram analysis and transformation for arbitrary programs,by providing high-level information to compilertransformations at compile-time, link-time, run-time, and inidle time between runs.LLVM defines a common, low-levelcode representation in Static Single Assignment (SSA) form,with several novel features: a simple, language-independenttype-system that exposes the primitives commonly used toimplement high-level language features; an instruction fortyped address arithmetic; and a simple mechanism that canbe used to implement the exception handling features ofhigh-level languages (and setjmp/longjmp in C) uniformlyand efficiently.The LLVM compiler framework and coderepresentation together provide a combination of key capabilitiesthat are important for practical, lifelong analysis andtransformation of programs.To our knowledge, no existingcompilation approach provides all these capabilities.We describethe design of the LLVM representation and compilerframework, and evaluate the design in three ways: (a) thesize and effectiveness of the representation, including thetype information it provides; (b) compiler performance forseveral interprocedural problems; and (c) illustrative examplesof the benefits LLVM provides for several challengingcompiler problems.},
isbn = {978-0-7695-2102-2},
series = {{{CGO}} '04},
venue = {Palo Alto, California}
}
@misc{rfc793,
author="J. Postel",
title="{Transmission Control Protocol}",
series="Request for Comments",
number="793",
howpublished="RFC 793 (Standard)",
publisher="IETF",
organisation="Internet Engineering Task Force",
year=1981,
month=sep,
day="1",
note="Updated by RFC 3168",
url="http://www.ietf.org/rfc/rfc793.txt",
}
@inproceedings{BR02,
author = {Ball, Thomas and Rajamani, Sriram K.},
title = {The {SLAM} project: debugging system software via static analysis},
booktitle = {Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
series = {POPL '02},
year = {2002},
isbn = {1-58113-450-9},
location = {Portland, Oregon},
pages = {1--3},
numpages = {3},
doi = {10.1145/503272.503274},
acmid = {503274},
publisher = {ACM},
address = {New York, NY, USA},
}
@inproceedings{CS04,
author = {Cantrill, Bryan M. and Shapiro, Michael W. and Leventhal, Adam H.},
title = {Dynamic instrumentation of production systems},
booktitle = {Proceedings of the USENIX Annual Technical Conference},
series = {ATEC '04},
year = {2004},
location = {Boston, MA},
pages = {2--2},
numpages = {1},
url = {http://portal.acm.org/citation.cfm?id=1247415.1247417},
acmid = {1247417},
publisher = {USENIX Association},
address = {Berkeley, CA, USA},
}
@inproceedings{HJ02,
Address = {London, UK},
Author = {Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and George C. Necula and Gr\&\#233;goire Sutre and Westley Weimer},
Booktitle = {Proceedings of the 14th International Conference on Computer Aided Verification (CAV)},
Date-Added = {2005-11-09 11:43:39 +0000},
Date-Modified = {2005-11-09 11:44:40 +0000},
Isbn = {3-540-43997-8},
Keywords = {security,systems},
Pages = {526--538},
Publisher = {Springer-Verlag},
Title = {Temporal-Safety Proofs for Systems Code},
Year = {2002}}
@TechReport{BP81,
author={K.H. Britton and D.L. Parnas},
Title={A-7E Software Module Guide},
institution= {NRL Memorandum Report 4702, Naval Research Laboratory},
address={Washington, D.C.}, month =dec, Year=1981 }
@InProceedings{CCMT93,
Author = "G. Canfora and A. Cimitile and M. Munro and C. Taylor",
Title = "Extracting Abstract Data Types from {C} Programs: {A} Case Study",
Booktitle = "Proceedings of the International Conference on Software
Maintenance",
Organization = "", Address = "", Year = "1993",
Pages="200--209", Month = sep }
@InProceedings{GK97,
Author = "J.F. Girard and R. Koschke",
Title = "Finding Components in a Hierarchy of Modules: A
Step Towards Architectural Understanding",
Booktitle = "Proceedings of the International Conference on Software
Maintenance",
Organization = "", Address = "", Year = "1997",
Pages="72--81", Month = oct }
@InProceedings{Gligor86,
Author={V.D. Gligor et al.},
Title={Design and Implementation of {Secure Xenix[TM]}},
BookTitle={Proceedings of the 1986 Symposium on Security and Privacy},
Organization={IEEE Computer Society}, Address={Oakland, California},
Year={1986}, Month=apr, pages={},
Note = {also in {\it IEEE Transactions on Software Engineering,} vol. SE-13, 2,
February 1987, 208--221}
}
@InProceedings{GM93,
Author={R. Godin and H. Mili},
Title={Building and Maintaining Analysis-Level Class
Hierarchies Using {Galois} Lattices},
BookTitle = {Proceedings of the 8th Annual Conference
on Object-Oriented Programming Systems, Languages and Applications
(OOPSLA '93), SIGPLAN Notices, 28, 10},
Year={1993},
Month={},
Pages={394--410}
}
@article{GMMMAC98,
Author={R. Godin and H. Mili and G.W. Mineau and R. Missaoui
and A. Arfi and T.-T. Chau},
Title={Design of Class Hierarchies Based on Concept {(Galois)} Lattices},
Journal = {Theory and Practice of Object Systems},
volume={4}, number={2}, year={1998}, pages={117-134}}
@Article{Hoare74,
Author = {C.A.R. Hoare},
Title = {Monitors: An Operating System Structuring Concept},
Journal = {Communications of the ACM},
Year = {1974},
Volume = {17},
Number = {10},
Pages = {},
Month = oct }
@InProceedings{Janson75,
Author={P.A. Janson},
Title={Dynamic Linking and Environment Initialization in a Multi-Domain Process},
BookTitle={Proceedings of the Fifth ACM Symposium on Operating Systems Principles},
Year={1975},
Month=nov,
Note={(ACM Operating Systems Review, Vol 9, No. 5)},
Pages = {43--50}
}
@Article{Janson81,
Author={P.A. Janson},
Journal={ACM Operating Systems Review},
Title={Using Type Extension to Organize Virtual Memory Mechanisms},
Year={1981},
Month=oct,
Pages={6--38},
Volume={15},
Number={4}
}
@InProceedings{LS97,
Author = "C. Lindig and G. Snelting",
Title = "Assessing Modular Structure of Legacy Code Based
On Mathematical Concept Analysis",
Booktitle = "Proceedings of the International Conference
on Software Engineering",
Organization = "", Address = "", Year = "1997",
Pages="349--359", Month = "" }
@ARTICLE{LJ94,
Author={P.E Livadas and T. Johnson},
TITLE = {A New Approach to finding Objects in Programs},
JOURNAL = {Software Maintenance: Research and Practice},
YEAR = {1994}, VOLUME = {6},
NUMBER = {}, PAGES = {249--260}, MONTH = {} }
@InProceedings{MMCG98,
Author = "S. Mancoridis and B.S. Mitchell and Y. Chen and E.R. Gansner",
Title = "Using Automatic
Clustering to produce High-Level System Organization of Source Code",
Booktitle = "Proceedings of the International Workshop on Program Comprehension",
Organization = "", Address = "", Year = "1998",
Pages="42--52", Month = "" }
@InProceedings{MMCG99,
Author = "S. Mancoridis and B.S. Mitchell and Y. Chen and E.R. Gansner",
Title = "Bunch: A Clustering Tool for the Recovery and Maintenance of
Software System Structures",
Booktitle = "Proceedings of the International Conference on Software
Maintenance",
Organization = "", Address = "", Year = "1999",
Pages="50--59", Month = "" }
@InProceedings{MH96,
Author = "S. Mancoridis and R.C. Holt",
Title = "Recovering the Structure of Software Systems
Using Tube Graph Interconnection Clustering",
Booktitle = "Proceedings of the International
Conference on Software Maintenance",
Organization = "", Address = "", Year = "1996",
Pages="23--32", Month = "" }
@InProceedings{MK88,
Author = "M.K. McKusick and M.J. Karels",
Title = "Design of a General Purpose Memory Allocator for the
{4.3BSD UNIX} Kernel",
Booktitle = "1988 Summer USENIX Conference Proceedings",
Organization = "", Address = "San Francisco, California", Year = "1988",
Pages="295--304", Month = jun }
@TechReport{Nelson81,
author={B.J. Nelson},
Title={Remote Procedure Call},
institution= {Research Report
CSL-79-9, XEROX Palo Alto Research Center},
address={3333 Coyote Hill Road,
Palo Alto, California}, month =may, Year=1981 }
@ARTICLE{Parnas79,
Author={D.L. Parnas},
TITLE = {Designing Software for Ease of Extension and Contraction},
JOURNAL = {IEEE Transactions on Software Engineering},
YEAR = {1979}, VOLUME = {SE-5},
NUMBER = {2}, PAGES = {128--138}, MONTH = mar }
@InProceedings{S91,
Author = "R.W. Schwanke",