skip to main content


Title: Proving confidentiality in a file system using DISKSEC
SFSCQ is the first file system with a machine-checked proof of security. To develop, specify, and prove SFSCQ, this paper introduces DiskSec, a novel approach for reasoning about confidentiality of storage systems, such as a file system. DiskSec addresses the challenge of specifying confidentiality using the notion of _data noninterference_ to find a middle ground between strong and precise information-flow-control guarantees and the weaker but more practical discretionary access control. DiskSec factors out reasoning about confidentiality from other properties (such as functional correctness) using a notion of _sealed blocks_. Sealed blocks enforce that the file system treats confidential file blocks as opaque in the bulk of the code, greatly reducing the effort of proving data noninterference. An evaluation of SFSCQ shows that its theorems preclude security bugs that have been found in real file systems, that DiskSec imposes little performance overhead, and that SFSCQ's incremental development effort, on top of DiskSec and DFSCQ, on which it is based, is moderate.  more » « less
Award ID(s):
1812522 1563763
NSF-PAR ID:
10099212
Author(s) / Creator(s):
; ; ; ;
Date Published:
Journal Name:
Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI)
Page Range / eLocation ID:
323-338
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. The behavior of large systems is guided by their configurations: users set parameters in the configuration file to dictate which corresponding part of the system code is executed. However, it is often the case that, although some parameters are set in the configuration file, they do not influence the system runtime behavior, thus failing to meet the user’s intent. Moreover, such misconfigurations rarely lead to an error message or raising an exception. We introduce the notion of silent misconfigurations which are prohibitively hard to identify due to (1) lack of feedback and (2) complex interactions between configurations and code. This paper presents ConfigX, the first tool for the detection of silent misconfigurations. The main challenge is to understand the complex interactions between configurations and the code that they affected. Our goal is to derive a specification describing non-trivial interactions between the configuration parameters that lead to silent misconfigurations. To this end, ConfigX uses static analysis to determine which parts of the system code are associated with configuration parameters. ConfigX then infers the connections between configuration parameters by analyzing their associated code blocks. We design customized control- and data-flow analysis to derive a specification of configurations. Additionally, we conduct reachability analysis to eliminate spurious rules to reduce false positives. Upon evaluation on five real-world datasets across three widely-used systems, Apache, vsftpd, and PostgreSQL, ConfigX detected more than 2200 silent misconfigurations. We additionally conducted a user study where we ran ConfigX on misconfigurations reported on user forums by real-world users. ConfigX easily detected issues and suggested repairs for those misconfigurations. Our solutions were accepted and confirmed in the interaction with the users, who originally posted the problems. 
    more » « less
  2. Nicewonger, Todd E. ; McNair, Lisa D. ; Fritz, Stacey (Ed.)
    https://pressbooks.lib.vt.edu/alaskanative/ At the start of the pandemic, the editors of this annotated bibliography initiated a remote (i.e., largely virtual) ethnographic research project that investigated how COVID-19 was impacting off-site modular construction practices in Alaska Native communities. Many of these communities are located off the road system and thus face not only dramatically higher costs but multiple logistical challenges in securing licensed tradesmen and construction crews and in shipping building supplies and equipment to their communities. These barriers, as well as the region’s long winters and short building seasons, complicate the construction of homes and related infrastructure projects. Historically, these communities have also grappled with inadequate housing, including severe overcrowding and poor-quality building stock that is rarely designed for northern Alaska’s climate (Marino 2015). Moreover, state and federal bureaucracies and their associated funding opportunities often further complicate home building by failing to accommodate the digital divide in rural Alaska and the cultural values and practices of Native communities.[1] It is not surprising, then, that as we were conducting fieldwork for this project, we began hearing stories about these issues and about how the restrictions caused by the pandemic were further exacerbating them. Amidst these stories, we learned about how modular home construction was being imagined as a possible means for addressing both the complications caused by the pandemic and the need for housing in the region (McKinstry 2021). As a result, we began to investigate how modular construction practices were figuring into emergent responses to housing needs in Alaska communities. We soon realized that we needed to broaden our focus to capture a variety of prefabricated building methods that are often colloquially or idiomatically referred to as “modular.” This included a range of prefabricated building systems (e.g., manufactured, volumetric modular, system-built, and Quonset huts and other reused military buildings[2]). Our further questions about prefabricated housing in the region became the basis for this annotated bibliography. Thus, while this bibliography is one of multiple methods used to investigate these issues, it played a significant role in guiding our research and helped us bring together the diverse perspectives we were hearing from our interviews with building experts in the region and the wider debates that were circulating in the media and, to a lesser degree, in academia. The actual research for each of three sections was carried out by graduate students Lauren Criss-Carboy and Laura Supple.[3] They worked with us to identify source materials and their hard work led to the team identifying three themes that cover intersecting topics related to housing security in Alaska during the pandemic. The source materials collected in these sections can be used in a variety of ways depending on what readers are interested in exploring, including insights into debates on housing security in the region as the pandemic was unfolding (2021-2022). The bibliography can also be used as a tool for thinking about the relational aspects of these themes or the diversity of ways in which information on housing was circulating during the pandemic (and the implications that may have had on community well-being and preparedness). That said, this bibliography is not a comprehensive analysis. Instead, by bringing these three sections together with one another to provide a snapshot of what was happening at that time, it provides a critical jumping off point for scholars working on these issues. The first section focuses on how modular housing figured into pandemic responses to housing needs. In exploring this issue, author Laura Supple attends to both state and national perspectives as part of a broader effort to situate Alaska issues with modular housing in relation to wider national trends. This led to the identification of multiple kinds of literature, ranging from published articles to publicly circulated memos, blog posts, and presentations. These materials are important source materials that will likely fade in the vastness of the Internet and thus may help provide researchers with specific insights into how off-site modular construction was used – and perhaps hyped – to address pandemic concerns over housing, which in turn may raise wider questions about how networks, institutions, and historical experiences with modular construction are organized and positioned to respond to major societal disruptions like the pandemic. As Supple pointed out, most of the material identified in this review speaks to national issues and only a scattering of examples was identified that reflect on the Alaskan context. The second section gathers a diverse set of communications exploring housing security and homelessness in the region. The lack of adequate, healthy housing in remote Alaska communities, often referred to as Alaska’s housing crisis, is well-documented and preceded the pandemic (Guy 2020). As the pandemic unfolded, journalists and other writers reported on the immense stress that was placed on already taxed housing resources in these communities (Smith 2020; Lerner 2021). The resulting picture led the editors to describe in their work how housing security in the region exists along a spectrum that includes poor quality housing as well as various forms of houselessness including, particularly relevant for the context, “hidden homelessness” (Hope 2020; Rogers 2020). The term houseless is a revised notion of homelessness because it captures a richer array of both permanent and temporary forms of housing precarity that people may experience in a region (Christensen et al. 2107). By identifying sources that reflect on the multiple forms of housing insecurity that people were facing, this section highlights the forms of disparity that complicated pandemic responses. Moreover, this section underscores ingenuity (Graham 2019; Smith 2020; Jason and Fashant 2021) that people on the ground used to address the needs of their communities. The third section provides a snapshot from the first year of the pandemic into how CARES Act funds were allocated to Native Alaska communities and used to address housing security. This subject was extremely complicated in Alaska due to the existence of for-profit Alaska Native Corporations and disputes over eligibility for the funds impacted disbursements nationwide. The resources in this section cover that dispute, impacts of the pandemic on housing security, and efforts to use the funds for housing as well as barriers Alaska communities faced trying to secure and use the funds. In summary, this annotated bibliography provides an overview of what was happening, in real time, during the pandemic around a specific topic: housing security in largely remote Alaska Native communities. The media used by housing specialists to communicate the issues discussed here are diverse, ranging from news reports to podcasts and from blogs to journal articles. This diversity speaks to the multiple ways in which information was circulating on housing at a time when the nightly news and radio broadcasts focused heavily on national and state health updates and policy developments. Finding these materials took time, and we share them here because they illustrate why attention to housing security issues is critical for addressing crises like the pandemic. For instance, one theme that emerged out of a recent National Science Foundation workshop on COVID research in the North NSF Conference[4] was that Indigenous communities are not only recovering from the pandemic but also evaluating lessons learned to better prepare for the next one, and resilience will depend significantly on more—and more adaptable—infrastructure and greater housing security. 
    more » « less
  3. We consider the problems of data maintenance on untrusted clouds. Specifically, two important use cases: (i) using public-key encryption to enforce dynamic access control, and (ii) efficient key rotation. Enabling access revocation is key to enabling dynamic access control, and proxy re-encryption and related technologies have been advocated as tools that allow for revocation on untrusted clouds. Regrettably, the literature assumes that data is encrypted directly with the primitives. Yet, for efficiency reasons hybrid encryption is used, and such schemes are susceptible to key-scraping attacks. For key rotation, currently deployed schemes have insufficient security properties, or are computationally quite intensive. Proposed systems are either still susceptible to key-scraping attacks, or too inefficient to deploy. We propose a new notion of security that is practical for both problems. We show how to construct hybrid schemes that are both resistant to key-scraping attacks and highly efficient in revocation or key rotation. The number of modifications to the ciphertext scales linearly with the security parameter and logarithmically with the file length. 
    more » « less
  4. Obeid, Iyad Selesnick (Ed.)
    Electroencephalography (EEG) is a popular clinical monitoring tool used for diagnosing brain-related disorders such as epilepsy [1]. As monitoring EEGs in a critical-care setting is an expensive and tedious task, there is a great interest in developing real-time EEG monitoring tools to improve patient care quality and efficiency [2]. However, clinicians require automatic seizure detection tools that provide decisions with at least 75% sensitivity and less than 1 false alarm (FA) per 24 hours [3]. Some commercial tools recently claim to reach such performance levels, including the Olympic Brainz Monitor [4] and Persyst 14 [5]. In this abstract, we describe our efforts to transform a high-performance offline seizure detection system [3] into a low latency real-time or online seizure detection system. An overview of the system is shown in Figure 1. The main difference between an online versus offline system is that an online system should always be causal and has minimum latency which is often defined by domain experts. The offline system, shown in Figure 2, uses two phases of deep learning models with postprocessing [3]. The channel-based long short term memory (LSTM) model (Phase 1 or P1) processes linear frequency cepstral coefficients (LFCC) [6] features from each EEG channel separately. We use the hypotheses generated by the P1 model and create additional features that carry information about the detected events and their confidence. The P2 model uses these additional features and the LFCC features to learn the temporal and spatial aspects of the EEG signals using a hybrid convolutional neural network (CNN) and LSTM model. Finally, Phase 3 aggregates the results from both P1 and P2 before applying a final postprocessing step. The online system implements Phase 1 by taking advantage of the Linux piping mechanism, multithreading techniques, and multi-core processors. To convert Phase 1 into an online system, we divide the system into five major modules: signal preprocessor, feature extractor, event decoder, postprocessor, and visualizer. The system reads 0.1-second frames from each EEG channel and sends them to the feature extractor and the visualizer. The feature extractor generates LFCC features in real time from the streaming EEG signal. Next, the system computes seizure and background probabilities using a channel-based LSTM model and applies a postprocessor to aggregate the detected events across channels. The system then displays the EEG signal and the decisions simultaneously using a visualization module. The online system uses C++, Python, TensorFlow, and PyQtGraph in its implementation. The online system accepts streamed EEG data sampled at 250 Hz as input. The system begins processing the EEG signal by applying a TCP montage [8]. Depending on the type of the montage, the EEG signal can have either 22 or 20 channels. To enable the online operation, we send 0.1-second (25 samples) length frames from each channel of the streamed EEG signal to the feature extractor and the visualizer. Feature extraction is performed sequentially on each channel. The signal preprocessor writes the sample frames into two streams to facilitate these modules. In the first stream, the feature extractor receives the signals using stdin. In parallel, as a second stream, the visualizer shares a user-defined file with the signal preprocessor. This user-defined file holds raw signal information as a buffer for the visualizer. The signal preprocessor writes into the file while the visualizer reads from it. Reading and writing into the same file poses a challenge. The visualizer can start reading while the signal preprocessor is writing into it. To resolve this issue, we utilize a file locking mechanism in the signal preprocessor and visualizer. Each of the processes temporarily locks the file, performs its operation, releases the lock, and tries to obtain the lock after a waiting period. The file locking mechanism ensures that only one process can access the file by prohibiting other processes from reading or writing while one process is modifying the file [9]. The feature extractor uses circular buffers to save 0.3 seconds or 75 samples from each channel for extracting 0.2-second or 50-sample long center-aligned windows. The module generates 8 absolute LFCC features where the zeroth cepstral coefficient is replaced by a temporal domain energy term. For extracting the rest of the features, three pipelines are used. The differential energy feature is calculated in a 0.9-second absolute feature window with a frame size of 0.1 seconds. The difference between the maximum and minimum temporal energy terms is calculated in this range. Then, the first derivative or the delta features are calculated using another 0.9-second window. Finally, the second derivative or delta-delta features are calculated using a 0.3-second window [6]. The differential energy for the delta-delta features is not included. In total, we extract 26 features from the raw sample windows which add 1.1 seconds of delay to the system. We used the Temple University Hospital Seizure Database (TUSZ) v1.2.1 for developing the online system [10]. The statistics for this dataset are shown in Table 1. A channel-based LSTM model was trained using the features derived from the train set using the online feature extractor module. A window-based normalization technique was applied to those features. In the offline model, we scale features by normalizing using the maximum absolute value of a channel [11] before applying a sliding window approach. Since the online system has access to a limited amount of data, we normalize based on the observed window. The model uses the feature vectors with a frame size of 1 second and a window size of 7 seconds. We evaluated the model using the offline P1 postprocessor to determine the efficacy of the delayed features and the window-based normalization technique. As shown by the results of experiments 1 and 4 in Table 2, these changes give us a comparable performance to the offline model. The online event decoder module utilizes this trained model for computing probabilities for the seizure and background classes. These posteriors are then postprocessed to remove spurious detections. The online postprocessor receives and saves 8 seconds of class posteriors in a buffer for further processing. It applies multiple heuristic filters (e.g., probability threshold) to make an overall decision by combining events across the channels. These filters evaluate the average confidence, the duration of a seizure, and the channels where the seizures were observed. The postprocessor delivers the label and confidence to the visualizer. The visualizer starts to display the signal as soon as it gets access to the signal file, as shown in Figure 1 using the “Signal File” and “Visualizer” blocks. Once the visualizer receives the label and confidence for the latest epoch from the postprocessor, it overlays the decision and color codes that epoch. The visualizer uses red for seizure with the label SEIZ and green for the background class with the label BCKG. Once the streaming finishes, the system saves three files: a signal file in which the sample frames are saved in the order they were streamed, a time segmented event (TSE) file with the overall decisions and confidences, and a hypotheses (HYP) file that saves the label and confidence for each epoch. The user can plot the signal and decisions using the signal and HYP files with only the visualizer by enabling appropriate options. For comparing the performance of different stages of development, we used the test set of TUSZ v1.2.1 database. It contains 1015 EEG records of varying duration. The any-overlap performance [12] of the overall system shown in Figure 2 is 40.29% sensitivity with 5.77 FAs per 24 hours. For comparison, the previous state-of-the-art model developed on this database performed at 30.71% sensitivity with 6.77 FAs per 24 hours [3]. The individual performances of the deep learning phases are as follows: Phase 1’s (P1) performance is 39.46% sensitivity and 11.62 FAs per 24 hours, and Phase 2 detects seizures with 41.16% sensitivity and 11.69 FAs per 24 hours. We trained an LSTM model with the delayed features and the window-based normalization technique for developing the online system. Using the offline decoder and postprocessor, the model performed at 36.23% sensitivity with 9.52 FAs per 24 hours. The trained model was then evaluated with the online modules. The current performance of the overall online system is 45.80% sensitivity with 28.14 FAs per 24 hours. Table 2 summarizes the performances of these systems. The performance of the online system deviates from the offline P1 model because the online postprocessor fails to combine the events as the seizure probability fluctuates during an event. The modules in the online system add a total of 11.1 seconds of delay for processing each second of the data, as shown in Figure 3. In practice, we also count the time for loading the model and starting the visualizer block. When we consider these facts, the system consumes 15 seconds to display the first hypothesis. The system detects seizure onsets with an average latency of 15 seconds. Implementing an automatic seizure detection model in real time is not trivial. We used a variety of techniques such as the file locking mechanism, multithreading, circular buffers, real-time event decoding, and signal-decision plotting to realize the system. A video demonstrating the system is available at: https://www.isip.piconepress.com/projects/nsf_pfi_tt/resources/videos/realtime_eeg_analysis/v2.5.1/video_2.5.1.mp4. The final conference submission will include a more detailed analysis of the online performance of each module. ACKNOWLEDGMENTS Research reported in this publication was most recently supported by the National Science Foundation Partnership for Innovation award number IIP-1827565 and the Pennsylvania Commonwealth Universal Research Enhancement Program (PA CURE). Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the official views of any of these organizations. REFERENCES [1] A. Craik, Y. He, and J. L. Contreras-Vidal, “Deep learning for electroencephalogram (EEG) classification tasks: a review,” J. Neural Eng., vol. 16, no. 3, p. 031001, 2019. https://doi.org/10.1088/1741-2552/ab0ab5. [2] A. C. Bridi, T. Q. Louro, and R. C. L. Da Silva, “Clinical Alarms in intensive care: implications of alarm fatigue for the safety of patients,” Rev. Lat. Am. Enfermagem, vol. 22, no. 6, p. 1034, 2014. https://doi.org/10.1590/0104-1169.3488.2513. [3] M. Golmohammadi, V. Shah, I. Obeid, and J. Picone, “Deep Learning Approaches for Automatic Seizure Detection from Scalp Electroencephalograms,” in Signal Processing in Medicine and Biology: Emerging Trends in Research and Applications, 1st ed., I. Obeid, I. Selesnick, and J. Picone, Eds. New York, New York, USA: Springer, 2020, pp. 233–274. https://doi.org/10.1007/978-3-030-36844-9_8. [4] “CFM Olympic Brainz Monitor.” [Online]. Available: https://newborncare.natus.com/products-services/newborn-care-products/newborn-brain-injury/cfm-olympic-brainz-monitor. [Accessed: 17-Jul-2020]. [5] M. L. Scheuer, S. B. Wilson, A. Antony, G. Ghearing, A. Urban, and A. I. Bagic, “Seizure Detection: Interreader Agreement and Detection Algorithm Assessments Using a Large Dataset,” J. Clin. Neurophysiol., 2020. https://doi.org/10.1097/WNP.0000000000000709. [6] A. Harati, M. Golmohammadi, S. Lopez, I. Obeid, and J. Picone, “Improved EEG Event Classification Using Differential Energy,” in Proceedings of the IEEE Signal Processing in Medicine and Biology Symposium, 2015, pp. 1–4. https://doi.org/10.1109/SPMB.2015.7405421. [7] V. Shah, C. Campbell, I. Obeid, and J. Picone, “Improved Spatio-Temporal Modeling in Automated Seizure Detection using Channel-Dependent Posteriors,” Neurocomputing, 2021. [8] W. Tatum, A. Husain, S. Benbadis, and P. Kaplan, Handbook of EEG Interpretation. New York City, New York, USA: Demos Medical Publishing, 2007. [9] D. P. Bovet and C. Marco, Understanding the Linux Kernel, 3rd ed. O’Reilly Media, Inc., 2005. https://www.oreilly.com/library/view/understanding-the-linux/0596005652/. [10] V. Shah et al., “The Temple University Hospital Seizure Detection Corpus,” Front. Neuroinform., vol. 12, pp. 1–6, 2018. https://doi.org/10.3389/fninf.2018.00083. [11] F. Pedregosa et al., “Scikit-learn: Machine Learning in Python,” J. Mach. Learn. Res., vol. 12, pp. 2825–2830, 2011. https://dl.acm.org/doi/10.5555/1953048.2078195. [12] J. Gotman, D. Flanagan, J. Zhang, and B. Rosenblatt, “Automatic seizure detection in the newborn: Methods and initial evaluation,” Electroencephalogr. Clin. Neurophysiol., vol. 103, no. 3, pp. 356–362, 1997. https://doi.org/10.1016/S0013-4694(97)00003-9. 
    more » « less
  5. Aim: With the widespread adoption of disk encryption technologies, it has become common for adversaries to employ coercive tactics to force users to surrender encryption keys. For some users, this creates a need for hidden volumes that provide plausible deniability, the ability to deny the existence of sensitive information. Previous deniable storage solutions only offer pieces of an implementable solution that do not take into account more advanced adversaries, such as intelligence agencies, and operational concerns. Specifically, they do not address an adversary that is familiar with the design characteristics of any deniable system. Methods: We evaluated existing threat models and deniable storage system designs to produce a new, stronger threat model and identified design characteristics necessary in a plausibly deniable storage system. To better explore the implications of this stronger adversary, we developed Artifice, the first tunable, operationally secure, self repairing, and fully deniable storage system. Results: With Artifice, hidden data blocks are split with an information dispersal algorithm such as Shamir Secret Sharing to produce a set of obfuscated carrier blocks that are indistinguishable from other pseudorandom blocks on the disk. The blocks are then stored in unallocated space of an existing file system. The erasure correcting capabilities of an information dispersal algorithm allow Artifice to self repair damage caused by writes to the public file system. Unlike preceding systems, Artifice addresses problems regarding flash storage devices and multiple snapshot attacks through simple block allocation schemes and operational security measures. To hide the user’s ability to run a deniable system and prevent information leakage, a user accesses Artifice through a separate OS stored on an external Linux live disk. Conclusion: In this paper, we present a stronger adversary model and show that our proposed design addresses the primary weaknesses of existing approaches to deniable storage under this stronger assumed adversary. 
    more » « less