Zobrazeno 1 - 10
of 17
pro vyhledávání: '"David Darais"'
Publikováno v:
Proceedings of the ACM on Programming Languages. 6:699-728
All current approaches for statically enforcing differential privacy in higher order languages make use of either linear or relational refinement types. A barrier to adoption for these approaches is the lack of support for expressing these "fancy typ
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::88b807db2ab2c94f20c510aa4a742366
https://doi.org/10.1145/3563313
https://doi.org/10.1145/3563313
Publikováno v:
CCS
Static program analysis tools can automatically prove many useful properties of programs. However, using static analysis to prove to a third party that a program satisfies a property requires revealing the program's source code. We introduce the conc
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d23cb670f094384c0a462044e6a9d103
https://doi.org/10.1145/3460120.3484795
https://doi.org/10.1145/3460120.3484795
Publikováno v:
Proceedings of the ACM on Programming Languages. 4:1-31
An oblivious computation is one that is free of direct and indirect information leaks, e.g., due to observable differences in timing and memory access patterns. This paper presents Lambda Obliv, a core language whose type system enforces obliviousnes
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::293d29b21b5bacb66fdcc86a4f03b6f1
https://doi.org/10.1145/3371118
https://doi.org/10.1145/3371118
Publikováno v:
CSF
Differential privacy enables general statistical analysis of data with formal guarantees of privacy protection at the individual level. Tools that assist data analysts with utilizing differential privacy have frequently taken the form of programming
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::055ad0dbcceca87bfa6f4ab9948e9ad3
https://doi.org/10.1109/csf51468.2021.00043
https://doi.org/10.1109/csf51468.2021.00043
Publikováno v:
Proceedings of the 15th Workshop on Programming Languages and Analysis for Security.
Memory-trace Obliviousness (MTO) is a noninterference property: programs that enjoy it have neither explicit nor implicit information leaks, even when the adversary can observe the program counter and the address trace of memory accesses. Probabilist
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::79d6347b19da02dab9f3017a20dd9a14
https://doi.org/10.1145/3411506.3417598
https://doi.org/10.1145/3411506.3417598
Publikováno v:
CSF
Authorization hooks are access control checks that prevent unauthorized principals from interacting with some protected resource, and are used extensively in critical software such as operating systems, middleware, and server programs. They are often
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b7ccd85ecb3b4c114bdfac95fdd34f04
https://doi.org/10.1109/csf49147.2020.00018
https://doi.org/10.1109/csf49147.2020.00018
Publikováno v:
CSF
Faceted execution is a linguistic paradigm for dynamic information-flow control with the distinguishing feature that program values may be faceted. Such values represent multiple versions or facets at once, for different security labels. This enables
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ab3c55c70c6435da30f9c299035b8091
https://doi.org/10.1109/csf49147.2020.00021
https://doi.org/10.1109/csf49147.2020.00021
Publikováno v:
Proceedings of the ACM on Programming Languages. 1:1-25
In this functional pearl, we examine the use of definitional interpreters as a basis for abstract interpretation of higher-order programming languages. As it turns out, definitional interpreters, especially those written in monadic style, can provide
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c1140bb448601a55bbd9c16969a1dc5e
https://doi.org/10.1145/3110256
https://doi.org/10.1145/3110256
Autor:
Matías Toro, David Darais, Chike Abuah, Joseph P. Near, Damián Árquez, Federico Olmedo, Éric Tanter
Language support for differentially-private programming is both crucial and delicate. While elaborate program logics can be very expressive, type-system based approaches using linear types tend to be more lightweight and amenable to automatic checkin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1712f87eb7e2399771c5b93ea1e3bc5c
Autor:
Joseph P. Near, Alex Shan, Pranav Gaddamadugu, David Darais, Dawn Song, Tim Stevens, Mu Zhang, Neel Somani, Chike Abuah, Nikhil Sharma, Lun Wang
During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides differential privacy often remains a manual task to be completed by an expert i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e67b0226330786370ad87a49dca0f51a