EDBT 2026 Demo / reviewers in the wild / expert
R. Sekar 0001
dblp:90/1136-1 · also R. C. Sekar 0001
· DBLP profile ↗
90ranked-venue papers
21as first author
7since 2021 · last 2026
0009-0008-9135-3296ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Security and privacy · 55 · 8 first-author · 4 since 2021Software engineering, systems software and programming languages · 20 · 6 first-author · 3 since 2021Systems, architecture and hardware · 11 · 1 since 2021Theory of computation · 9 · 6 first-authorArtificial intelligence and machine learning · 1 · 1 first-authorComputer networks · 1 · 1 first-authorHuman-computer interaction and ubiquitous computing · 1Applied, interdisciplinary, general and emerging computing · 1 · 1 first-author
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Sealing the Window: Efficient Tamper Protection for Provenance Logs
Sagar Mishra, R. Sekar 0001 |
SP | 2 |
| 2026 | Analyzing Bytes: Pre-Disassembly Static Binary AnalysisabstractBinary code analysis plays a central role in numerous applications in software security, performance optimization, reverse engineering, and so on. Existing techniques need to first disassemble binaries into functions in assembly code before an analysis can be performed. However, disassembly and function identification have proven to be major challenges for complex variable-length instruction sets such as the x86. A recent trend has been to use static analysis to improve the accuracy of these tasks. This raises a chicken-and-egg problem: a disassembly is needed for static analysis, but a static analysis is needed for accurate disassembly! We overcome this problem by developing a novel static analysis approach that can operate before committing to a disassembly. Our analysis operates on the output of exhaustive disassembly that considers each possible offset in a binary as an instruction, and constructs what is known as a super-set control-flow graph (CFG). The central technical challenge in analyzing this CFG is that it mixes legitimate instructions with unintended ones, causing analysis results from invalid code paths to pollute legitimate ones. To overcome this challenge, we begin with a key new insight that if we focus on backward analyses, we can ensure accuracy of analysis results at intended instructions even though we have no idea where these intended instructions are! Moreover, our analysis operates in time that is linear in the size of the binary. Specifically, in O(n) total time, it yields analysis results for every one of the n offsets in an n-byte binary. For this task, it is orders of magnitude faster than previous techniques, as the previous techniques typically need to repeat the analysis many times. Huan Nguyen 0004, Soumyakant Priyadarshan, Chencheng Jiang, R. Sekar 0001 |
Proc. ACM Program. Lang. | 4 |
| 2025 | Incorporating Gradients to Rules: Towards Lightweight, Adaptive Provenance-based Intrusion Detection
Lingzhi Wang 0002, Xiangmin Shen, Weijian Li 0002, Zhenyuan Li, R. Sekar 0001, Han Liu 0001, Yan Chen 0004 |
NDSS | 5 |
| 2024 | Scalable, Sound, and Accurate Jump Table AnalysisabstractJump tables are a common source of indirect jumps in binary code. Resolving these indirect jumps is critical for constructing a complete control-flow graph, which is an essential first step for most applications involving binaries, including binary hardening and instrumentation, binary analysis and fuzzing for vulnerability discovery, malware analysis and reverse engineering. Existing techniques for jump table analysis generally prioritize performance over soundness. While lack of soundness may be acceptable for applications such as decompilation, it can cause unpredictable runtime failures in binary instrumentation applications. We therefore present SJA, a new jump table analysis technique in this paper that is sound and scalable. Our analysis uses a novel abstract domain to systematically track the "structure" of computed code pointers without relying on syntactic pattern-matching that is common in previous works. In addition, we present a bounds analysis that efficiently and losslessly reasons about equality and inequality relations that arise in the context of jump tables. As a result, our system reduces miss rate by 35× over the next best technique. When evaluated on error rate based on F1-score, our technique outperforms the best previous techniques by 3×. Huan Nguyen 0004, Soumyakant Priyadarshan, R. Sekar 0001 |
ISSTA | 3 |
| 2024 | eAudit: A Fast, Scalable and Deployable Audit Data Collection SystemabstractToday’s advanced cyber attack campaigns can often bypass all existing protections. The primary defense against them is after-the-fact detection, followed by a forensic analysis to understand their impact. Such an analysis requires audit logs (also called provenance logs) that faithfully capture all activities and data flows on each host. While the Linux auditing daemon (auditd) and sysdig are the most popular tools for audit data collection, a number of other systems, authored by researchers and practitioners, are also available. Through a motivating experimental study, we show that these systems impose high overheads, slowing workloads by 2× to 8×; lose a majority of events under sustained workloads; and are vulnerable to log tampering that erases log entries before they are committed to persistent storage. We present a new approach that overcomes these challenges. By relying on the extended Berkeley Packet Filter (eBPF) framework built into recent Linux versions, we avoid changes to the kernel code, and hence our data collector works out of the box on most Linux distributions. We present new design, tuning and optimization techniques that enables our system to sustain workloads that are an order of magnitude more intense than those causing major data loss with existing systems. Moreover, our system incurs only a fraction of the overhead of previous systems, while considerably reducing data volumes, and shrinking the log tampering window by ~ 100×. R. Sekar 0001, Hanke Kimm, Rohit Aich |
SP | 1 |
| 2023 | Accurate Disassembly of Complex Binaries Without Use of Compiler MetadataabstractAccurate disassembly of stripped binaries is the first step in binary analysis, instrumentation and reverse engineering. Complex instruction sets such as the x86 pose major challenges in this context because it is very difficult to distinguish between code and embedded data. To make progress, many recent approaches have either made optimistic assumptions (e.g., absence of embedded data) or relied on additional compiler-generated metadata (e.g., relocation info and/or exception handling metadata). Unfortunately, many complex binaries do contain embedded data, while lacking the additional metadata needed by these techniques. We therefore present a novel approach for accurate disassembly that uses statistical properties of data to detect code, and behavioral properties of code to flag data. We present new static analysis and data-driven probabilistic techniques that are then combined using a prioritized error correction algorithm to achieve results that are 3X to 4X more accurate than the best previous results. Soumyakant Priyadarshan, Huan Nguyen 0004, R. Sekar 0001 |
ASPLOS (4) | 3 |
| 2023 | SAFER: Efficient and Error-Tolerant Binary Instrumentation
Soumyakant Priyadarshan, Huan Nguyen 0004, Rohit Chouhan, R. Sekar 0001 |
USENIX Security Symposium | 4 |
| 2020 | Practical Fine-Grained Binary Code Randomization†abstractDespite its effectiveness against code reuse attacks, fine-grained code randomization has not been deployed widely due to compatibility as well as performance concerns. Previous techniques often needed source code access to achieve good performance, but this breaks compatibility with today’s binary-based software distribution and update mechanisms. Moreover, previous techniques break C++ exceptions and stack tracing, which are crucial for practical deployment. In this paper, we first propose a new, tunable randomization technique called LLR(k) that is compatible with these features. Since the metadata needed to support exceptions/stack-tracing can reveal considerable information about code layout, we propose a new entropy metric that accounts for leaks of this metadata. We then present a novel metadata reduction technique to significantly increase entropy without degrading exception handling. This enables LLR(k) to achieve strong entropy with a low overhead of 2.26%. Soumyakant Priyadarshan, Huan Nguyen 0004, R. Sekar 0001 |
ACSAC | 3 |
| 2020 | Combating Dependence Explosion in Forensic Analysis Using Alternative Tag Propagation SemanticsabstractWe are witnessing a rapid escalation in targeted cyber-attacks called Advanced and Persistent Threats (APTs). Carried out by skilled adversaries, these attacks take place over extended time periods, and remain undetected for months. A common approach for retracing the attacker's steps is to start with one or more suspicious events from system logs, and perform a dependence analysis to uncover the rest of attacker's actions. The accuracy of this analysis suffers from the dependence explosion problem, which causes a very large number of benign events to be flagged as part of the attack. In this paper, we propose two novel techniques, tag attenuation and tag decay, to mitigate dependence explosion. Our techniques take advantage of common behaviors of benign processes, while providing a conservative treatment of processes and data with suspicious provenance. Our system, called Morse, is able to construct a compact scenario graph that summarizes attacker activity by sifting through millions of system events in a matter of seconds. Our experimental evaluation, carried out using data from two government-agency sponsored red team exercises, demonstrates that our techniques are (a) effective in identifying stealthy attack campaigns, (b) reduce the false alarm rates by more than an order of magnitude, and (c) yield compact scenario graphs that capture the vast majority of the attack, while leaving out benign background activity. Md Nahid Hossain, Sanaz Sheikhi, R. Sekar 0001 |
SP | 3 |
| 2019 | HOLMES: Real-Time APT Detection through Correlation of Suspicious Information FlowsabstractIn this paper, we present HOLMES, a system that implements a new approach to the detection of Advanced and Persistent Threats (APTs). HOLMES is inspired by several case studies of real-world APTs that highlight some common goals of APT actors. In a nutshell, HOLMES aims to produce a detection signal that indicates the presence of a coordinated set of activities that are part of an APT campaign. One of the main challenges addressed by our approach involves developing a suite of techniques that make the detection signal robust and reliable. At a high-level, the techniques we develop effectively leverage the correlation between suspicious information flows that arise during an attacker campaign. In addition to its detection capability, HOLMES is also able to generate a high-level graph that summarizes the attacker's actions in real-time. This graph can be used by an analyst for an effective cyber response. An evaluation of our approach against some real-world APTs indicates that HOLMES can detect APT campaigns with high precision and low false alarm rate. The compact high-level graphs produced by HOLMES effectively summarizes an ongoing attack campaign and can assist real-time cyber-response operations. Sadegh M. Milajerdi, Rigel Gjomemo, Birhanu Eshete, R. Sekar 0001, V. N. Venkatakrishnan |
IEEE Symposium on Security and Privacy | 4 |
| 2018 | Dependence-Preserving Data Compaction for Scalable Forensic Analysis
Md Nahid Hossain, Junao Wang, R. Sekar 0001, Scott D. Stoller |
USENIX Security Symposium | 3 |
| 2017 | Protecting COTS Binaries from Disclosure-guided Code Reuse AttacksabstractCode diversification, combined with execute-only memory, provides an effective defense against just-in-time code reuse attacks. However, existing techniques for combining code diversification and hardware-assisted memory protections typically require compiler support, as well as the deployment or modification of a hypervisor. These requirements often cannot be met, either because source code is not available, or because the required hardware features may not be available on the target system. In this paper we present SECRET, a software hardening technique tailored to legacy and closed-source software that provides equivalent protection to execute-only memory without relying on hardware features or recompilation. This is achieved using two novel techniques, code space isolation and code pointer remapping, which prevent read accesses to the executable memory of the protected code. Furthermore, SECRET thwarts code pointer harvesting attacks on ELF files by remapping existing code pointers to use random values. SECRET has been implemented on 32-bit Linux systems. Our evaluation shows that it introduces just 2% additional runtime overhead on top of a state-of-the-art CFI implementation, bringing the total average overhead to about 16%. In addition, it achieves better protection coverage compared to compiler-based techniques, as it can handle low-level machine code such as inline assembly or extra code introduced by the linker and loader. Mingwei Zhang 0005, Michalis Polychronakis, R. Sekar 0001 |
ACSAC | 3 |
| 2017 | Function Interface Analysis: A Principled Approach for Function Recognition in COTS BinariesabstractFunction recognition is one of the key tasks in binary analysis, instrumentation and reverse engineering. Previous approaches for this problem have relied on matching code patterns commonly observed at the beginning and end of functions. While early efforts relied on compiler idioms and expert-identified patterns, more recent works have systematized the process using machine-learning techniques. In contrast, we develop a novel static analysis based method in this paper. In particular, we combine a low-level technique for enumerating candidate functions with a novel static analysis for determining if these candidates exhibit the properties associated with a function interface. Both control-flow properties (e.g., returning to the location at the stack top at the function entry point) and data-flow properties (e.g., parameter passing via registers and the stack, and the degree of adherence to application-binary interface conventions) are checked. Our approach achieves an F1-score above 99% across a broad range of programs across multiple languages and compilers. More importantly, it achieves a 4x or higher reduction in error rate over best previous results. Rui Qiao 0002, R. Sekar 0001 |
DSN | 2 |
| 2017 | SLEUTH: Real-time Attack Scenario Reconstruction from COTS Audit Data
Md Nahid Hossain, Sadegh M. Milajerdi, Junao Wang, Birhanu Eshete, Rigel Gjomemo, R. Sekar 0001, Scott D. Stoller, V. N. Venkatakrishnan |
USENIX Security Symposium | 6 |
| 2016 | Lifting Assembly to Intermediate Representation: A Novel Approach Leveraging CompilersabstractTranslating low-level machine instructions into higher-level intermediate language (IL) is one of the central steps in many binary analysis and instrumentation systems. Existing systems build such translators manually. As a result, it takes a great deal of effort to support new architectures. Even for widely deployed architectures, full instruction sets may not be modeled, e.g., mature systems such as Valgrind still lack support for AVX, FMA4 and SSE4.1 for x86 processors. To overcome these difficulties, we propose a novel approach that leverages knowledge about instruction set semantics that is already embedded into modern compilers such as GCC. In particular, we present a learning-based approach for automating the translation of assembly instructions to a compiler's architecture-neutral IL. We present an experimental evaluation that demonstrates the ability of our approach to easily support many architectures (x86, ARM and AVR), including their advanced instruction sets. Our implementation is available as open-source software. Niranjan Hasabnis, R. Sekar 0001 |
ASPLOS | 2 |
| 2016 | Hardening OpenStack Cloud Platforms against Compute Node CompromisesabstractInfrastructure-as-a-Service (IaaS) clouds such as OpenStack consist of two kinds of nodes in their infrastructure: control nodes and compute nodes. While control nodes run all critical services, compute nodes host virtual machines of customers. Given the large number of compute nodes, and the fact that they are hosting VMs of (possibly malicious) customers, it is possible that some of the compute nodes may be compromised. This paper examines the impact of such a compromise. We focus on OpenStack, a popular open-source cloud plat- form that is widely adopted. We show that attackers com- promising a single compute node can extend their controls over the entire cloud infrastructure. They can then gain free access to resources that they have not paid for, or even bring down the whole cloud to affect all customers. This startling result stems from the cloud platform's misplaced trust, which does not match today's threats. To overcome the weakness, we propose a new system, called SOS , for hardening OpenStack. SOS limits trust on compute nodes. SOS consists of a framework that can enforce a wide range of security policies. Specifically, we applied mandatory access control and capabilities to con- fine interactions among different components. Effective confinement policies are generated automatically. Furthermore, SOS requires no modifications to the OpenStack. This has allowed us to deploy SOS on multiple versions of OpenStack. Our experimental results demonstrate that SOS is scalable, incurs negligible overheads and offers strong protection. Wai-Kit Sze, Abhinav Srivastava, R. Sekar 0001 |
AsiaCCS | 3 |
| 2016 | Extracting instruction semantics via symbolic execution of code generatorsabstractBinary analysis and instrumentation form the basis of many tools and frameworks for software debugging, security hardening, and monitoring. Accurate modeling of instruction semantics is paramount in this regard, as errors can lead to program crashes, or worse, bypassing of security checks. Semantic modeling is a daunting task for modern processors such as x86 and ARM that support over a thousand instructions, many of them with complex semantics. This paper describes a new approach to automate this semantic modeling task. Our approach leverages instruction semantics knowledge that is already encoded into today's production compilers such as GCC and LLVM. Such an approach can greatly reduce manual effort, and more importantly, avoid errors introduced by manual modeling. Furthermore, it is applicable to any of the numerous architectures already supported by the compiler. In this paper, we develop a new symbolic execution technique to extract instruction semantics from a compiler's source code. Unlike previous applications of symbolic execution that were focused on identifying a single program path that violates a property, our approach addresses the all paths problem, extracting the entire input/output behavior of the code generator. We have applied it successfully to the 120K lines of C-code used in GCC's code generator to extract x86 instruction semantics. To demonstrate architecture-neutrality, we have also applied it to AVR, a processor used in the popular Arduino platform. Niranjan Hasabnis, R. Sekar 0001 |
SIGSOFT FSE | 2 |
| 2016 | Condition Factorization: A Technique for Building Fast and Compact Packet Matching AutomataabstractRule-based matching on network packet headers is a central problem in firewalls, and network intrusion, monitoring, and access-control systems. To enhance performance, rules are typically compiled into a matching automaton that can quickly identify the subset of rules that are applicable to a given network packet. While deterministic automata provide the best performance, previous research has shown that such automata can be exponential in the size and/or number of rules. Nondeterministic automata can avoid size explosion, but their matching time can increase quickly with the number of rules. In contrast, we present a new technique that constructs polynomial size automata. Moreover, we show that the matching time of our automata is insensitive to the number of rules. The key idea in our approach is that of decomposing and reordering the tests on packet header fields so that the result of performing a test can be utilized on behalf of many rules. Our experiments demonstrate major reductions in space requirements over previous techniques, as well as significant improvements in matching speed. Our technique can uniformly handle prioritized and unprioritized rules, and support applications that require single-match as well as multi-match. Alok Tongaonkar, R. Sekar 0001 |
IEEE Trans. Inf. Forensics Secur. | 2 |
| 2015 | A Principled Approach for ROP DefenseabstractReturn-Oriented Programming (ROP) is an effective attack technique that can escape modern defenses such as DEP. ROP is based on repeated abuse of existing code snippets ending with return instructions (called gadgets), as compared to using injected code. Several defense mechanisms have been proposed to counter ROP by enforcing policies on the targets of return instructions, and/or their frequency. However, these policies have been repeatedly bypassed by more advanced ROP attacks. While stricter policies have the potential to thwart ROP, they lead to incompatibilities which discourage their deployment. In this work, we address this challenge by presenting a principled approach for ROP defense. Our experimental evaluation shows that our approach enforces a strong policy, while offering better compatibility and good performance. Rui Qiao 0002, Mingwei Zhang 0005, R. Sekar 0001 |
ACSAC | 3 |
| 2015 | Provenance-based Integrity Protection for WindowsabstractExisting malware defenses are primarily reactive in nature, with defenses effective only on malware that has previously been observed. Unfortunately, we are witnessing a generation of stealthy, highly targeted exploits and malware that these defenses are unprepared for. Thwarting such malware requires new defenses that are, by design, secure against unknown malware. In this paper, we present Spif, an approach that defends against malware by tracking code and data origin, and ensuring that any process that is influenced by code or data from untrusted sources will be prevented from modifying important system resources, and interacting with benign processes. Spif is designed for Windows, the most widely deployed desktop OS, and the primary platform targeted by malware. Spif is compatible with all recent Windows versions (Windows XP to Windows 10), and supports a wide range of feature rich, unmodified applications, including all popular browsers, office software and media players. Spif imposes minimal performance overheads while being able to stop a variety of malware attacks, including Stuxnet and the recently reported Sandworm malware. An open-source implementation of our system is available. Wai-Kit Sze, R. Sekar 0001 |
ACSAC | 2 |
| 2015 | JaTE: Transparent and Efficient JavaScript ConfinementabstractInclusion of third-party scripts is a common practice, even among major sites handling sensitive data. The default browser security policies are ill-suited for securing web sites from vulnerable or malicious third-party scripts: the choice is between full privilege ( ) and isolation ( ), with nearly all use cases (advertisement, libraries, analytics, etc.) requiring the former. Previous work attempted to bridge the gap between the two alternatives, but all the solutions were plagued by one or more of the following problems: (a) lack of compatibility, causing most existing third-party scripts to fail (b) excessive performance overheads, and (c) not supporting object-level policies. For these reasons, confinement of JavaScript code suitable for widespread deployment is still an open problem. Our solution, JaTE, has none of the above shortcomings. In contrast, our approach can be deployed on today's web sites, while imposing a relatively low overhead of about 20%, even on web pages that include about a megabyte of minified JavaScript code. Tung Tran 0003, Riccardo Pelizzi, R. Sekar 0001 |
ACSAC | 3 |
| 2015 | Control Flow and Code Integrity for COTS binaries: An Effective Defense Against Real-World ROP AttacksabstractDespite decades of sustained effort, memory corruption attacks continue to be one of the most serious security threats faced today. They are highly sought after by attackers, as they provide ultimate control --- the ability to execute arbitrary low-level code. Attackers have shown time and again their ability to overcome widely deployed countermeasures such as Address Space Layout Randomization (ASLR) and Data Execution Prevention (DEP) by crafting Return Oriented Programming (ROP) attacks. Although Turing-complete ROP attacks have been demonstrated in research papers, real-world ROP payloads have had a more limited objective: that of disabling DEP so that injected native code attacks can be carried out. In this paper, we provide a systematic defense, called Control Flow and Code Integrity (CFCI), that makes injected native code attacks impossible. CFCI achieves this without sacrificing compatibility with existing software, the need to replace system programs such as the dynamic loader, and without significant performance penalty. We will release CFCI as open-source software by the time of this conference. Mingwei Zhang 0005, R. Sekar 0001 |
ACSAC | 2 |
| 2015 | Checking correctness of code generator architecture specificationsabstractModern instruction sets are complex, and extensions are proposed to them frequently. This makes the task of modelling architecture specifications used by the code generators of modern compilers complex and error-prone. Given the important role played by the compilers, it is necessary that they are tested thoroughly, so that most of the bugs are detected early on. Unfortunately, modern compilers such as GCC do not target testing of individual components of a compiler, but instead perform end-to-end testing. In this paper, we target the problem of checking correctness of the architecture specifications used by code generators of modern compilers. Our solution leverages the architecture of modern compilers where a language-specific front-end compiles source-code into an intermediate representation (IR), which is then translated by the compiler's code generator into assembly code. Hence our approach is to test code generators by testing the equivalence of IR snippets and the corresponding assembly code generated. For this purpose, we have developed an efficient, architecture-neutral test case generation strategy. Using our prototype implementation, we performed correctness checking of 140 assembly instructions (80 general-purpose and 60 SSE out of around 600×86 instructions) of GCC's ×86 code generator, and found semantic differences in 39 of them, at least one of which has already been fixed by the GCC community in response to our report. We believe that our approach can be invaluable when developing support for a new architecture, as well as during frequent updates made to existing architectures such as ×86 for the purpose of supporting new instructions. Niranjan Hasabnis, Rui Qiao 0002, R. Sekar 0001 |
CGO | 3 |
| 2015 | WebSheets: Web Applications for Non-ProgrammersabstractSpreadsheets are a very successful programming paradigm. Their success stems from user's familiarity with tabular data, and their previous experience in performing manual computations on such data. Since tabular data is familiar to users in the context of web applications as well, we propose WebSheets, a new paradigm for developing web applications using a spreadsheet-like language. WebSheets can enable simple web applications to be developed without "programming," in much the same way that non-programmers create budgets or expense reports using spreadsheets. More importantly, WebSheets enable users to express fine-grained privacy policies on their data in a simple manner, thus putting them in charge of their own privacy and security concerns. Riccardo Pelizzi, R. Sekar 0001 |
NSPW | 2 |
| 2014 | Code-Pointer Integrity
Volodymyr Kuznetsov, Laszlo Szekeres, Mathias Payer, George Candea, R. Sekar 0001, Dawn Song |
OSDI | 5 |
| 2014 | Towards more usable information flow policies for contemporary operating systemsabstractThere has been a resurgence of interest in information flow based techniques in security. A key attraction of these techniques is that they can provide strong, principled protection against malware, regardless of its sophistication. In spite of this advantage, most advances in information flow control have not been adopted in mainstream operating systems since a strict application of information flow can limit system functionality and usability. Permitting dynamic changes to subject labels, as proposed in the low-watermark model, provides better usability. However, it suffers from the self-revocation problem, whereby read/write operations on already open files are denied because the label of the subject performing these operations has been downgraded. While most applications deal gracefully with security failures on file open operations, they are unprepared to handle security violations on subsequent reads/writes. As a result, subject downgrades may lead to crashes or malfunction. Even those applications that deal with read/write errors may still leave output files in a corrupted or inconsistent state since write permissions were taken away in the midst of producing an output file. To overcome these drawbacks, we propose a new approach for dynamic downgrading that eliminates the self-revocation problem. We show that our approach represents an optimal combination of functionality and compatibility. Our experimental evaluation shows that our approach is efficient, incurring an overhead of a few percentage points, is compatible with existing applications, and provides strong integrity protection. Wai-Kit Sze, Bhuvan Mital, R. Sekar 0001 |
SACMAT | 3 |
| 2014 | Comprehensive integrity protection for desktop linuxabstractInformation flow provides principled defenses against malware. It can provide system-wide integrity protection without requiring any program-specific understanding. Information flow policies have been around for 40+ years but they have not been explored in today's context. Specifically, they are not designed for contemporary software and OSes. Applying these policies directly on today's OSes affects usability. In this paper, we focus our attention on an information-flow based integrity protection system that we implemented for Linux, with the goal of minimizing usability impact. We discuss the design decisions made in this system and provide insights on building usable information flow systems. Wai-Kit Sze, R. Sekar 0001 |
SACMAT | 2 |
| 2014 | A platform for secure static binary instrumentationabstractProgram instrumentation techniques form the basis of many recent software security defenses, including defenses against common exploits and security policy enforcement. As compared to source-code instrumentation, binary instrumentation is easier to use and more broadly applicable due to the ready availability of binary code. Two key features needed for security instrumentations are (a) it should be applied to all application code, including code contained in various system and application libraries, and (b) it should be non-bypassable. So far, dynamic binary instrumentation (DBI) techniques have provided these features, whereas static binary instrumentation (SBI) techniques have lacked them. These features, combined with ease of use, have made DBI the de facto choice for security instrumentations. However, DBI techniques can incur high overheads in several common usage scenarios, such as application startups, system-calls, and many real-world applications. We therefore develop a new platform for secure static binary instrumentation (PSI) that overcomes these drawbacks of DBI techniques, while retaining the security, robustness and ease-of-use features. We illustrate the versatility of PSI by developing several instrumentation applications: basic block counting, shadow stack defense against control-flow hijack and return-oriented programming attacks, and system call and library policy enforcement. While being competitive with the best DBI tools on CPU-intensive SPEC 2006 benchmark, PSI provides an order of magnitude reduction in overheads on a collection of real-world applications. Mingwei Zhang 0005, Rui Qiao 0002, Niranjan Hasabnis, R. Sekar 0001 |
VEE | 4 |
| 2013 | A portable user-level approach for system-wide integrity protectionabstractIn this paper, we develop an approach for protecting system integrity from untrusted code that may harbor sophisticated malware. We develop a novel dual-sandboxing architecture to confine not only untrusted, but also benign processes. Our sandboxes place only a few restrictions, thereby permitting most applications to function normally. Our implementation is performed entirely at the user-level, requiring no changes to the kernel. This enabled us to port the system easily from Linux to BSD. Our experimental results show that our approach preserves the usability of applications, while offering strong protection and good performance. Moreover, policy development is almost entirely automated, sparing users and administrators this cumbersome and difficult task. Wai-Kit Sze, R. Sekar 0001 |
ACSAC | 2 |
| 2013 | Control Flow Integrity for COTS Binaries
Mingwei Zhang 0005, R. Sekar 0001 |
USENIX Security Symposium | 2 |
| 2012 | Protection, usability and improvements in reflected XSS filtersabstractDue to the high popularity of Cross-Site Scripting (XSS) attacks, most major browsers now include or support filters to protect against reflected XSS attacks. Internet Explorer and Google Chrome provide built-in filters, while Firefox supports extensions that provide this functionality. However, these filters all have limitations. Riccardo Pelizzi, R. Sekar 0001 |
AsiaCCS | 2 |
| 2012 | Light-weight bounds checkingabstractMemory errors in C and C++ programs continue to be one of the dominant sources of security problems, accounting for over a third of the high severity vulnerabilities reported in 2011. Wide-spread deployment of defenses such as address-space layout randomization (ASLR) have made memory exploit development more difficult, but recent trends indicate that attacks are evolving to overcome this defense. Techniques for systematic detection and blocking of memory errors can provide more comprehensive protection that can stand up to skilled adversaries, but unfortunately, these techniques introduce much higher overheads and provide significantly less compatibility than ASLR. We propose a new memory error detection technique that explores a part of the design space that trades off some ability to detect bounds errors in order to obtain good performance and excellent backwards compatibility. On the SPECINT 2000 benchmark, the runtime overheads of our technique is about half of that reported by the fastest previous bounds-checking technique. On the compatibility front, our technique has been tested on over 7 million lines of code, which is much larger than that reported for previous bounds-checking techniques. Niranjan Hasabnis, Ashish Misra, R. Sekar 0001 |
CGO | 3 |
| 2011 | A server- and browser-transparent CSRF defense for web 2.0 applicationsabstractCross-Site Request Forgery (CSRF) vulnerabilities constitute one of the most serious web application vulnerabilities, ranking fourth in the CWE/SANS Top 25 Most Dangerous Software Errors. By exploiting this vulnerability, an attacker can submit requests to a web application using a victim user's credentials. A successful attack can lead to compromised accounts, stolen bank funds or information leaks. This paper presents a new server-side defense against CSRF attacks. Our solution, called jCSRF, operates as a serverside proxy, and does not require any server or browser modifications. Thus, it can be deployed by a site administrator without requiring access to web application source code, or the need to understand it. Moreover, protection is achieved without requiring web-site users to make use of a specific browser or a browser plug-in. Unlike previous server-side solutions, jCSRF addresses two key aspects of Web 2.0: extensive use of client-side scripts that can create requests to URLs that do not appear in the HTML page returned to the client; and services provided by two or more collaborating web sites that need to make cross-domain requests. Riccardo Pelizzi, R. Sekar 0001 |
ACSAC | 2 |
| 2011 | Information Flow Containment: A Practical Basis for Malware Defense
R. Sekar 0001 |
DBSec | 1 |
| 2010 | PAriCheck: an efficient pointer arithmetic checker for C programsabstractBuffer overflows are still a significant problem in programs written in C and C++. In this paper we present a bounds checker, called PAriCheck, that inserts dynamic runtime checks to ensure that attackers are not able to abuse buffer overflow vulnerabilities. The main approach is based on checking pointer arithmetic rather than pointer dereferences when performing bounds checks. The checks are performed by assigning a unique label to each object and ensuring that the label is associated with each memory location that the object inhabits. Whenever pointer arithmetic occurs, the label of the base location is compared to the label of the resulting arithmetic. If the labels differ, an out-of-bounds calculation has occurred. Benchmarks show that PAriCheck has a very low performance overhead compared to similar bounds checkers. This paper demonstrates that using bounds checkers for programs or parts of programs running on high-security production systems is a realistic possibility. Yves Younan, Pieter Philippaerts, Lorenzo Cavallaro, R. Sekar 0001, Frank Piessens, Wouter Joosen |
AsiaCCS | 4 |
| 2010 | Runtime Analysis and Instrumentation for Securing Software
R. Sekar 0001 |
RV | 1 |
| 2009 | Fast Packet Classification Using Condition Factorization
Alok Tongaonkar, R. Sekar 0001, Sreenaath Vasudevan |
ACNS | 2 |
| 2009 | Online Signature Generation for Windows SystemsabstractIn this paper, we present a new, light-weight approach for generating filters for blocking buffer overflow attacks on Microsoft Windows systems. It is designed to be deployable as an "always on'' component on production systems. To achieve this goal, it avoids expensive and intrusive techniques such as taint-tracking. The online nature of our system enables it to provide protection from a range of memory corruption exploits, including those involving unknown vulnerabilities, or known vulnerabilities but unknown exploits. In contrast, most previous signature generation techniques need to be run in sandboxed environments, and need working exploits to generate signatures. Moreover, our technique overcomes the "gap'' problem faced by previous signature generation mechanisms, i.e., when the vulnerable memory region is corrupted between the overflow and the time an attack is detected. Another novel feature of our approach is that it is able to reason about likely lengths of vulnerable buffers, which can lead to more accurate signatures. Our experimental results are very promising, and demonstrate that the approach can generate effective signatures for many synthetic and real-world vulnerabilities. James E. Just, R. Sekar 0001 |
ACSAC | 3 |
| 2009 | An Efficient Black-box Technique for Defeating Web Application Attacks
R. Sekar 0001 |
NDSS | 1 |
| 2009 | Alcatraz: An Isolated Environment for Experimenting with Untrusted SoftwareabstractIn this article, we present an approach for realizing a safe execution environment (SEE) that enables users to “try out” new software (or configuration changes to existing software) without the fear of damaging the system in any manner. A key property of our SEE is that it faithfully reproduces the behavior of applications, as if they were running natively on the underlying (host) operating system. This is accomplished via one-way isolation: processes running within the SEE are given read-access to the environment provided by the host OS, but their write operations are prevented from escaping outside the SEE. As a result, SEE processes cannot impact the behavior of host OS processes, or the integrity of data on the host OS. SEEs support a wide range of tasks, including: study of malicious code, controlled execution of untrusted software, experimentation with software configuration changes, testing of software patches, and so on. It provides a convenient way for users to inspect system changes made within the SEE. If these changes are not accepted, they can be rolled back at the click of a button. Otherwise, the changes can be committed so as to become visible outside the SEE. We provide consistency criteria that ensure semantic consistency of the committed results. We develop two different implementation approaches, one in user-land and the other in the OS kernel , for realizing a safe-execution environment. Our implementation results show that most software, including fairly complex server and client applications, can run successfully within our SEEs. It introduces low performance overheads, typically below 10 percent. Zhenkai Liang, Weiqing Sun, V. N. Venkatakrishnan, R. Sekar 0001 |
ACM Trans. Inf. Syst. Secur. | 4 |
| 2008 | A practical mimicry attack against powerful system-call monitorsabstractSystem-call monitoring has become the basis for many hostbased intrusion detection as well as policy enforcement techniques. Mimicry attacks attempt to evade system-call monitoring IDS by executing innocuous-looking sequences of system calls that accomplish the attacker’s goals. Mimicry attacks may execute a sequence of dozens of system calls in order to evade detection. Finding such a sequence is difficult, so researchers have focused on tools for automating mimicry attacks and extending them to gray-box IDS 1. In this paper, we describe an alternative approach for building mimicry attacks using only skills and technologies that hackers possess today, making this attack a more immediate and realistic threat. These attacks, which we call persistent interposition attacks, are not as powerful as traditional mimicry attacks — an adversary cannot obtain a root shell using a persistent interposition attack — but are sufficient to accomplish the goals of today’s cyber-criminals. Persistent interposition attacks are stealthier than standard mimicry attacks and are amenable to covert information-harvesting attacks, features that are likely to be attractive to profitmotivated criminals. Persistent interposition attacks are not IDS specific — they can evade a large class of systemcall-monitoring intrusion-detection systems, which we call I/O-data-oblivious. I/O-data-oblivious monitors have perfect knowledge of the values of all system call arguments as well as their relationships, with the exception of data buffer arguments to read and write. Many of today’s black-box and gray-box IDS are I/O-data-oblivious and hence vulnerable to persistent interposition attacks. Chetan Parampalli, R. Sekar 0001, Rob Johnson 0001 |
AsiaCCS | 2 |
| 2008 | Efficient fine-grained binary instrumentationwith applications to taint-trackingabstractFine-grained binary instrumentations, such as those for taint-tracking, have become very popular in computer security due to their applications in exploit detection, sandboxing, malware analysis, etc. However, practical application of taint-tracking has been limited by high performance overheads. For instance, previous software based techniques for taint-tracking on binary code have typically slowed down programs by a factor of 3 or more. In contrast, source-code based techniques have achieved better performance using high level optimizations. Unfortunately, these optimizations are difficult to perform on binaries since much of the high level program structure required by such static analyses is lost during the compilation process. In this paper, we address this challenge by developing static techniques that can recover some of the higher level structure from x86 binaries. Our new static analysis enables effective optimizations, which are applied in the context of taint tracking. As a result, we achieve a substantial reduction in performance overheads as compared to previous works. Prateek Saxena, R. Sekar 0001, Varun Puranik |
CGO | 2 |
| 2008 | Data Space Randomization
Sandeep Bhatkar, R. Sekar 0001 |
DIMVA | 2 |
| 2008 | On the Limits of Information Flow Techniques for Malware Analysis and Containment
Lorenzo Cavallaro, Prateek Saxena, R. Sekar 0001 |
DIMVA | 3 |
| 2008 | Expanding Malware Defense by Securing Software Installations
Weiqing Sun, R. Sekar 0001, Zhenkai Liang, V. N. Venkatakrishnan |
DIMVA | 2 |
| 2008 | Fast Packet Classification for Snort by Native Compilation of Rules
Alok Tongaonkar, Sreenaath Vasudevan, R. Sekar 0001 |
LISA | 3 |
| 2008 | Anomalous Taint Detection
Lorenzo Cavallaro, R. Sekar 0001 |
RAID | 2 |
| 2008 | The role of virtualization in computing educationabstractOver the past years, many problems related to the system administration of laboratories for undergraduate system-oriented courses have found elegant solutions in the deployment of virtualization suites. This technological advance enabled these courses to switch from a mostly descriptive content to learning activities which engage students in hands-on, authentic, problem-based learning. Since this type of activity requires students to be administrators of their own virtual machines (VM) or even virtual networks, the experience gained is intrinsically authentic. The potential impact on student learning, as compared to simulation or lecture only based setups is worth investigating for laboratories in operating systems, networking, computer security, system administration, etc. Alessio Gaspar, Sarah Langevin, William D. Armitage, R. Sekar 0001, Thomas Daniels 0001 |
SIGCSE | 4 |
| 2008 | Practical Proactive Integrity Preservation: A Basis for Malware DefenseabstractUnlike today's reactive approaches, information flow based approaches can provide positive assurances about overall system integrity, and hence can defend against sophisticated malware. However, there hasn't been much success in applying information flow based techniques to desktop systems running modern COTS operating systems. This is, in part, due to the fact that a strict application of information flow policy can break existing applications and OS services. Another important factor is the difficulty of policy development, which requires us to specify integrity labels for hundreds of thousands of objects on the system. This paper develops a new approach for proactive integrity protection that overcomes these challenges by decoupling integrity labels from access policies. We then develop an analysis that can largely automate the generation of integrity labels and policies that preserve the usability of applications in most cases. Evaluation of our prototype implementation on a Linux desktop distribution shows that it does not break or inconvenience the use of most applications, while stopping a variety of sophisticated malware attacks. Weiqing Sun, R. Sekar 0001, Gaurav Poothia, Tejas Karandikar |
SP | 2 |
| 2007 | Inferring Higher Level Policies from Firewall Rules
Alok Tongaonkar, Niranjan Inamdar, R. Sekar 0001 |
LISA | 3 |
| 2006 | Address-Space Randomization for Windows SystemsabstractAddress-space randomization (ASR) is a promising solution to defend against memory corruption attacks that have contributed to about three-quarters of USCERT advisories in the past few years. Several techniques have been proposed for implementing ASR on Linux, but its application to Microsoft Windows, the largest monoculture on the Internet, has not received as much attention. We address this problem in this paper and describe a solution that provides about 15-bits of randomness in the locations of all (code or data) objects. Our randomization is applicable to all processes on a Windows box, including all core system services, as well as applications such as web browsers, office applications, and so on. Our solution has been deployed continuously for about a year on a desktop system used daily, and is robust enough for production use. James E. Just, R. Sekar 0001 |
ACSAC | 3 |
| 2006 | Provably Correct Runtime Enforcement of Non-interference Properties
V. N. Venkatakrishnan, Daniel C. DuVarney, R. Sekar 0001 |
ICICS | 4 |
| 2006 | A Framework for Building Privacy-Conscious Composite Web ServicesabstractThe rapid growth of Web applications has prompted increasing interest in the area of composite Web services that involve several service providers. The potential for such composite Web services can be realized only if consumer privacy concerns are satisfactorily addressed. In this paper, we propose a framework that addresses consumer privacy concerns in the context of highly customizable composite Web services. Our approach involves service producers exchanging their terms-of-use with consumers in the form of "models". Our framework provides automated techniques for checking these models at the consumer site for compliance of consumer privacy policies. In the event of a policy violation, our framework supports automatic generation of "obligations" that the consumer generates for the composite service. These obligations are automatically enforced through a dynamic program analysis approach on the Web service composition code. We illustrate our approach with the implementation of two example services V. N. Venkatakrishnan, R. Sekar 0001, I. V. Ramakrishnan |
ICWS | 3 |
| 2006 | Dataflow Anomaly DetectionabstractBeginning with the work of Forrest et al, several researchers have developed intrusion detection techniques based on modeling program behaviors in terms of system calls. A weakness of these techniques is that they focus on control flows involving system calls, but not their arguments. This weakness makes them susceptible to several classes of attacks, including attacks on security-critical data, race-condition and symbolic link attacks, and mimicry attacks. To address this weakness, we develop a new approach for learning dataflow behaviors of programs. The novelty in our approach, as compared to previous system-call argument learning techniques, is that it learns temporal properties involving the arguments of different system calls, thus capturing the flow of security-sensitive data through the program. An interesting aspect of our technique is that it can be uniformly layered on top of most existing control-flow models, and can leverage control-flow contexts to significantly increase the precision of dataflows captured by the model. This contrasts with previous system-call argument learning techniques that did not leverage control-flow information, and moreover, were focused on learning statistical properties of individual system call arguments. Through experiments, we show that temporal properties enable detection of many attacks that aren't detected by previous approaches. Moreover, they support formal reasoning about security assurances that can be provided when a program follows its dataflow behavior model, e.g., tar would read only files located within a directory specified as a command-line argument. Sandeep Bhatkar, Abhishek Chaturvedi, R. Sekar 0001 |
S&P | 3 |
| 2006 | Taint-Enhanced Policy Enforcement: A Practical Approach to Defeat a Wide Range of Attacks
Sandeep Bhatkar, R. Sekar 0001 |
USENIX Security Symposium | 3 |
| 2005 | Automatic Generation of Buffer Overflow Attack Signatures: An Approach Based on Program Behavior ModelsabstractBuffer overflows have become the most common target for network-based attacks. They are also the primary mechanism used by worms and other forms of automated attacks. Although many techniques have been developed to prevent server compromises due to buffer overflows, these defenses still lead to server crashes. When attacks occur repeatedly, as is common with automated attacks, these protection mechanisms lead to repeated restarts of the victim application, rendering its service unavailable. To overcome this problem, we develop a new approach that can learn the characteristics of a particular attack, and filter out future instances of the same attack or its variants. By doing so, our approach significantly increases the availability of servers subjected to repeated attacks. The approach is fully automatic, does not require source code, and has low runtime overheads. In our experiments, it was effective against most attacks, and did not produce any false positives. Zhenkai Liang, R. Sekar 0001 |
ACSAC | 2 |
| 2005 | Fast and automated generation of attack signatures: a basis for building self-protecting serversabstractLarge-scale attacks, such as those launched by worms and zombie farms, pose a serious threat to our network-centric society. Existing approaches such as software patches are simply unable to cope with the volume and speed with which new vulnerabilities are being discovered. In this paper, we develop a new approach that can provide effective protection against a vast majority of these attacks that exploit memory errors in C/C++ programs. Our approach, called COVERS, uses a forensic analysis of a victim server's memory to correlate attacks to inputs received over the network, and automatically develop a signature that characterizes inputs that carry attacks. The signatures tend to capture characteristics of the underlying vulnerability (e.g., a message field being too long) rather than the characteristics of an attack, which makes them effective against variants of attacks. Our approach introduces low overheads (under 10%), does not require access to source code of the protected server, and has successfully generated signatures for the attacks studied in our experiments, without producing false positives. Since the signatures are generated in tens of milliseconds, they can potentially be distributed quickly over the Internet to filter out (and thus stop) fast-spreading worms. Another interesting aspect of our approach is that it can defeat guessing attacks reported against address-space randomization and instruction set randomization techniques. Finally, it increases the capacity of servers to withstand repeated attacks by a factor of 10 or more. Zhenkai Liang, R. Sekar 0001 |
CCS | 2 |
| 2005 | One-Way Isolation: An Effective Approach for Realizing Safe Execution Environments
Weiqing Sun, Zhenkai Liang, V. N. Venkatakrishnan, R. Sekar 0001 |
NDSS | 4 |
| 2005 | Automatic Synthesis of Filters to Discard Buffer Overflow Attacks: A Step Towards Realizing Self-Healing Systems
Zhenkai Liang, R. Sekar 0001, Daniel C. DuVarney |
USENIX ATC, General Track | 2 |
| 2004 | An efficient and backwards-compatible transformation to ensure memory safety of C programsabstractMemory-related errors, such as buffer overflows and dangling pointers, remain one of the principal reasons for failures of C programs. As a result, a number of recent research efforts have focused on the problem of dynamic detection of memory errors in C programs. However, existing approaches suffer from one or more of the following problems: inability to detect all memory errors (e.g., Purify), requiring non-trivial modifications to existing C programs (e.g., Cyclone), changing the memory management model of C to use garbage collection (e.g., CCured), and excessive performance overheads. In this paper, we present a new approach that addresses these problems. Our approach operates via source code transformation and combines efficient data-structures with simple, localized optimizations to obtain good performance. Daniel C. DuVarney, R. Sekar 0001 |
SIGSOFT FSE | 3 |
| 2003 | Isolated Program Execution: An Application Transparent Approach for Executing Untrusted ProgramsabstractWe present a new approach for safe execution of untrusted programs by isolating their effects from the rest of the system. Isolation is achieved by intercepting file operations made by untrusted processes, and redirecting any change operations to a "modification cache" that is invisible to other processes in the system. File read operations performed by the untrusted process are also correspondingly modified, so that the process has a consistent view of system state that incorporates the contents of the file system as well as the modification cache. On termination of the untrusted process, its user is presented with a concise summary of the files modified by the process. Additionally, the user can inspect these files using various software utilities (e.g., helper applications to view multimedia files) to determine if the modifications are acceptable. The user then has the option to commit these modifications, or simply discard them. Essentially, our approach provides "play" and "rewind" buttons for running untrusted software. Key benefits of our approach are that it requires no changes to the untrusted programs (to be isolated) or the underlying operating system; it cannot be subverted by malicious programs; and it achieves these benefits with acceptable runtime overheads. We describe a prototype implementation of this system for Linux called Alcatraz and discuss its performance and effectiveness. Zhenkai Liang, V. N. Venkatakrishnan, R. Sekar 0001 |
ACSAC | 3 |
| 2003 | An Approach for Detecting Self-propagating Email Using Anomaly Detection
Ajay Gupta 0002, R. Sekar 0001 |
RAID | 2 |
| 2003 | Model-carrying code: a practical approach for safe execution of untrusted applications
R. Sekar 0001, V. N. Venkatakrishnan, Samik Basu 0001, Sandeep Bhatkar, Daniel C. DuVarney |
SOSP | 1 |
| 2003 | Address Obfuscation: An Efficient Approach to Combat a Broad Range of Memory Error Exploits
Sandeep Bhatkar, Daniel C. DuVarney, R. Sekar 0001 |
USENIX Security Symposium | 3 |
| 2002 | Specification-based anomaly detection: a new approach for detecting network intrusionsabstractUnlike signature or misuse based intrusion detection techniques, anomaly detection is capable of detecting novel attacks. However, the use of anomaly detection in practice is hampered by a high rate of false alarms. Specification-based techniques have been shown to produce a low rate of false alarms, but are not as effective as anomaly detection in detecting novel attacks, especially when it comes to network probing and denial-of-service attacks. This paper presents a new approach that combines specification-based and anomaly-based intrusion detection, mitigating the weaknesses of the two approaches while magnifying their strengths. Our approach begins with state-machine specifications of network protocols, and augments these state machines with information about statistics that need to be maintained to detect anomalies. We present a specification language in which all of this information can be captured in a succinct manner. We demonstrate the effectiveness of the approach on the 1999 Lincoln Labs intrusion detection evaluation data, where we are able to detect all of the probing and denial-of-service attacks with a low rate of false alarms (less than 10 per day). Whereas feature selection was a crucial step that required a great deal of expertise and insight in the case of previous anomaly detection approaches, we show that the use of protocol specifications in our approach simplifies this problem. Moreover, the machine learning component of our approach is robust enough to operate without human supervision, and fast enough that no sampling techniques need to be employed. As further evidence of effectiveness, we present results of applying our approach to detect stealthy email viruses in an intranet environment. R. Sekar 0001, Ajay Gupta 0002, J. Frullo, T. Shanbhag, A. Tiwari |
CCS | 1 |
| 2002 | An Approach for Secure Software Installation
V. N. Venkatakrishnan, R. Sekar 0001, T. Kamat, S. Tsipa, Zhenkai Liang |
LISA | 2 |
| 2002 | Empowering mobile code using expressive security policiesabstractExisting approaches for mobile code security tend to take a conservative view that mobile code is inherently risky, and hence focus on confining it. Such confinement is usually achieved using access control policies that restrict mobile code from taking any action that can potentially be used to harm the host system. While such policies can be helpful in keeping "bad applets" in check, they preclude a large number of useful applets. We therefore take an alternative view of mobile code security, one that is focused on empowering mobile code rather than disabling it. We propose an approach wherein highly expressive security policies provide the basis for such empowerment, while greatly mitigating the risks posed to the host system by such code. Our policies are represented as extended finite state automata, (a generalization of the finite-state automata to permit the use of variables) that can enforce these policies efficiently. We have built a prototype implementation of our approach for Java. Our implementation is based on rewriting Java byte code so that security-relevant events are intercepted and forwarded to the policy enforcement automata before they are executed. Early experimental results indicate that such expressive, enabling policies can be supported with low overheads. V. N. Venkatakrishnan, Ram Peri, R. Sekar 0001 |
NSPW | 3 |
| 2002 | Model-Based Analysis of Configuration VulnerabilitiesabstractVulnerability analysis is concerned with the problem of identifying weaknesses in computer systems that can be exploited to compromise their security. In this paper we describe a new approach to vulnerability analysis based on model checking. Our approach involves: Formal specification of desired security properties. An example of such a property is “no ordinary user can overwrite system log files”.An abstract model of the system that captures its security-related behaviors. This model is obtained by composing models of system components such as the file system, privileged processes, etc.A verification procedure that checks whether the abstract model satisfies the security properties, and if not, produces execution sequences (also called exploit scenarios) that lead to a violation of these properties. An important benefit of a model-based approach is that it can be used to detect known and as-yet-unknown vulnerabilities. This capability contrasts with previous approaches (such as those used in COPS and SATAN) which mainly address known vulnerabilities. This paper demonstrates our approach by modelling a simplified version of a UNIX-based system, and analyzing this system using model-checking techniques to identify nontrivial vulnerabilities. A key contribution of this paper is to show that such an automated analysis is feasible in spite of the fact that the system models are infinite-state systems. Our techniques exploit some of the latest techniques in model-checking, such as constraint-based (implicit) representation of state-space, together with domain-specific optimizations that are appropriate in the context of vulnerability analysis. Clearly, a realistic UNIX system is much more complex than the one that we have modelled in this paper. Nevertheless, we believe that our results show automated and systematic vulnerability analysis of realistic systems to be feasible in the near future, as model-checking techniques continue to improve. C. R. Ramakrishnan 0001, R. Sekar 0001 |
J. Comput. Secur. | 2 |
| 2001 | Model-Carrying Code (MCC): a new paradigm for mobile-code securityabstractA new approach for ensuring the security of mobile code is proposed. Our approach enables a mobile-code consumer to understand and formally reason about what a piece of mobile code can do; check if the actions of the code are compatible with his/her security policies; and, if so, execute the code. The compatibility-checking process is automated, but if there are conflicts, consumers have the opportunity to refine their policies, taking into account the functionality provided by the mobile code. Finally, when the code is executed, our framework uses runtime-monitoring techniques to ensure that the code does not violate the consumer's (refined) policies.At the heart of our method, which we call model-carrying code (MCC), is the idea that a piece of mobile code comes equipped with an expressive yet concise model of the code's (security-relevant) behavior. The generation of such models can be automated. MCC enjoys several advantages over current approaches to mobile-code security. It protects consumers of mobile code from malicious or faulty code without unduly restricting the code's functionality. Also, it is applicable to the vast majority of code that exists today, which is written in C or C++. This contrasts with previous approaches such as Java 2 security and proof-carrying code, which are either language-specific or are limited to type-safe languages. Finally, MCC can be combined with existing techniques such as cryptographic signing and proof-carrying code to yield additional benefits. R. Sekar 0001, C. R. Ramakrishnan 0001, I. V. Ramakrishnan, Scott A. Smolka |
NSPW | 1 |
| 2001 | Experiences with Specification-Based Intrusion Detection
Premchand Uppuluri, R. Sekar 0001 |
Recent Advances in Intrusion Detection | 2 |
| 2001 | A Fast Automaton-Based Method for Detecting Anomalous Program BehaviorsabstractAnomaly detection on system call sequences has become perhaps the most successful approach for detecting novel intrusions. A natural way for learning sequences is to use a finite-state automaton (FSA). However previous research indicates that FSA-learning is computationally expensive, that it cannot be completely automated or that the space usage of the FSA may be excessive. We present a new approach that overcomes these difficulties. Our approach builds a compact FSA in a fully automatic and efficient manner, without requiring access to source code for programs. The space requirements for the FSA is low - of the order of a few kilobytes for typical programs. The FSA uses only a constant time per system call during the learning as well as the detection period. This factor leads to low overheads for intrusion detection. Unlike many of the previous techniques, our FSA-technique can capture both short term and long term temporal relationships among system calls, and thus perform more accurate detection. This enables our approach to generalize and predict future behaviors from past behaviors. As a result, the training periods needed for our FSA based approach are shorter. Moreover false positives are reduced without increasing the likelihood of missing attacks. This paper describes our FSA based technique and presents a comprehensive experimental evaluation of the technique. R. Sekar 0001, M. Bendre, D. Dhurjati, P. Bollineni |
S&P | 1 |
| 2001 | Automata-driven efficient subterm unification
R. Ramesh 0001, I. V. Ramakrishnan, R. Sekar 0001 |
Theor. Comput. Sci. | 3 |
| 2000 | User-Level Infrastructure for System Call Interposition: A Platform for Intrusion Detection and Confinement
K. Jain, R. Sekar 0001 |
NDSS | 2 |
| 1999 | A High-Performance Network Intrusion Detection SystemabstractIn this paper we present a new approach for network intrusion detection based on concise specifications that characterize normal and abnormal network packet sequences. Our specification language is geared for a robust network intrusion detection by enforcing a strict type discipline via a combination of static and dynamic type checking. Unlike most previous approaches in network intrusion detection, our approach can easily support new network protocols as information relating to the protocols are not hard-coded into the system. Instead, we simply add suitable type definitions in the specifications and define intrusion patterns on these types. We compile these specifications into a high-performance network intrusion detection system. Important components of our approach include efficient algorithms for pattern-matching and information aggregation on sequences of network packets. In particular, our techniques ensure that the matching time is insensitive to the number of patterns characterizing different network intrusions, and that the aggregation operations typically take constant time per packet. Our system participated in an intrusion detection evaluation organized by MIT Lincoln Labs, where our system demonstrated its effectiveness (96% detection rate on low-level network attacks) and performance (real-time detection at 500Mbps), while producing very few false positives (0.05 to 0.1 per attack). R. Sekar 0001, Y. Guang, S. Verma, T. Shanbhag |
CCS | 1 |
| 1999 | Synthesizing Fast Intrusion Prevention/Detection Systems from High-Level Specifications
R. Sekar 0001, Premchand Uppuluri |
USENIX Security Symposium | 1 |
| 1997 | On the power and limitations of strictness analysisabstractStrictness analysis is an important technique for optimization of lazy functional languages. It is well known that all strictness analysis methods are incomplete , i.e., fail to report some strictness properties. In this paper, we provide a precise and formal characterization of the loss of information that leads to this incompletenss. Specifically, we establish the following characterization theorem for Mycroft's strictness analysis method and a generalization of this method, called ee-analysis , that reasons about exhaustive evaluation in nonflat domains: Mycroft's method will deduce a strictness property for program P iff the property is independent of any constant appearing in any evaluation of P. To prove this, we specify a small set of equations, called E-axioms , that capture the information loss in Mycroft's method and develop a new proof technique called E-rewriting . E -rewriting extends the standard notion of rewriting to permit the use of reductions using E -axioms interspersed with standard reduction steps. E -axioms are a syntactic characterization of information loss and E -rewriting provides and algorithm-independent proof technique for characterizing the power of analysis methods. It can be used to answer questions on completeness and incompleteness of Mycroft's method on certain natural classes of programs. Finally, the techniques developed in this paper provide a general principle for establishing similar results for other analysis methods such as those based on abstract interpretation. As a demonstration of the generality of our technique, we give a characterization theorem for another variation of Mycroft's method called dd -analysis. R. Sekar 0001, I. V. Ramakrishnan, Prateek Mishra |
J. ACM | 1 |
| 1997 | EQUALS - A Fast Parallel Implementation of a Lazy LanguageabstractThis paper describes E QUALS , a fast parallel implementation of a lazy functional language on a commercially available shared-memory parallel machine, the Sequent Symmetry. In contrast to previous implementations, we propagate normal form demand at compile time as well as run time, and detect parallelism automatically using strictness analysis. The E QUALS implementation indicates the effectiveness of NF-demand propagation in identifying significant parallelism and in achieving good sequential as well as parallel performance. Another important difference between E QUALS and previous implementations is the use of reference counting for memory management, instead of mark-and-sweep or copying garbage collection. Implementation results show that reference counting leads to very good scalability and low memory requirements, and offers sequential performance comparable to generational garbage collectors. We compare the performance of E QUALS with that of other parallel implementations (the 〈 v , G 〉-machine and GAML) as well as with the performance of SML/NJ, a sequential implementation of a strict language. Owen Kaser, C. R. Ramakrishnan 0001, I. V. Ramakrishnan, R. Sekar 0001 |
J. Funct. Program. | 4 |
| 1995 | A Symbolic Constraint Solving Framework for Analysis of Logic ProgramsabstractInterpretation of logic programs using symbolic constraints has attracted a lot of attention lately since such layers that enables us to modularize not only our algorithms and implementations, but also the proof efforts.Prototype implementation of our framework shows that it scales very well to large domains, and furthermore, compares favorably with existing implementations of other analysis methods. C. R. Ramakrishnan 0001, I. V. Ramakrishnan, R. Sekar 0001 |
PEPM | 3 |
| 1995 | Adaptive Pattern MatchingabstractPattern matching is an important operation used in many applications such as functional programming, rewriting, and rule-based expert systems. By preprocessing the patterns into a deterministic finite state automaton, we can rapidly select the matching pattern(s) in a single scan of the relevant portions of the input term. This automaton is typically based on left-to-right traversal of the patterns. By adapting the traversal order to suit the set of input patterns, it is possible to considerably reduce the space and matching time requirements of the automaton. The design of such adaptive automata is the focus of this paper. We first formalize the notion of an adaptive traversal. We then present several strategies for synthesizing adaptive traversal orders aimed at reducing space and matching time complexity. In the worst case, however, the space requirements can be exponential in the size of the patterns. We show this by establishing an exponential lower bound on space that is independent of the traversal order used. We then discuss an orthogonal approach to space minimization based on direct construction of optimal directed acyclic graph (dag) automata. Finally, our work stresses the impact of typing in pattern matching. In particular, we show that several important problems (e.g., lazy pattern matching in ML) are computationally difficult in the presence of type disciplines, whereas they can be solved efficiently in the untyped setting. R. Sekar 0001, R. Ramesh 0001, I. V. Ramakrishnan |
SIAM J. Comput. | 1 |
| 1995 | Fast Strictness Analysis Based on Demand PropagationabstractStrictnessanalysis is a well-known technique used in compilers for optimization of sequential and '90.. R. Sekar 0001, I. V. Ramakrishnan |
ACM Trans. Program. Lang. Syst. | 1 |
| 1994 | Modelling techniques for evolving distributed applications
R. Sekar 0001, Yow-Jian Lin, C. R. Ramakrishnan 0001 |
FORTE | 1 |
| 1994 | Automata-Driven Efficient Subterm Unification
R. Ramesh 0001, I. V. Ramakrishnan, R. Sekar 0001 |
FSTTCS | 3 |
| 1993 | Extracting Determinacy in Logic Programs
Steven Dawson, C. R. Ramakrishnan 0001, I. V. Ramakrishnan, R. Sekar 0001 |
ICLP | 4 |
| 1993 | Programming in Equational Logic: Beyond Strong Sequentiality
R. Sekar 0001, I. V. Ramakrishnan |
Inf. Comput. | 1 |
| 1992 | Programming with Equations: A Framework for Lazy Parallel Evaluation
R. Sekar 0001, I. V. Ramakrishnan |
CADE | 1 |
| 1992 | Adaptive Pattern Matching
R. Sekar 0001, R. Ramesh 0001, I. V. Ramakrishnan |
ICALP | 1 |
| 1991 | On the Power and Limitation of Strictness Analysis Based on Abstract InterpretationabstractStrictness analysis based on abstract interpretation is an important technique for optimization of lazy functional languages.It is well known that all strictness analysis methods are incomplete, i.e., fail to report some strictness properties.In this paper, we provide the first precise and formal characterization of the loss of information that leads to this incompleteness.Specifically, we establish the following characterization theorem for Mycroft's method called old-analysis. R. Sekar 0001, Prateek Mishra, I. V. Ramakrishnan |
POPL | 1 |
| 1990 | Programming in Equational Logic: Beyond Strong SequentialityabstractThe authors consider whether it is possible to devise a complete normalization algorithm that minimizes (rather than eliminates) the wasteful reductions for the entire class of regular systems. A solution is proposed to this problem using the concept of a necessary set of redexes. In such a set, at least one of the redexes must be reduced to normalize a term. An algorithm is devised to compute a necessary set for any term not in normal form, and it is shown that a strategy that repeatedly reduces all redexes in such a set is complete for regular programs. It is also shown that the algorithm is optimal among all normalization algorithms that are based on left-hand sides alone. This means that the algorithm is lazy (like Huet-Levy's) on strongly sequential parts of a program, relaxes laziness minimally to handle the other parts, and thus does not sacrifice generality for the sake of efficiency.> R. Sekar 0001, I. V. Ramakrishnan |
LICS | 1 |
| 1990 | Small Domains Spell Fast Strictness AnalysisabstractUse of strictness analysis in parallel evaluation and optimization of lazy functional languages is well known. The first formal treatment of strictness analysis appeared in Mycroft's seminal work which however dealt only with flat domains. Unlike flat domains, strictness analysis on non-flat domains involves determining how a function transforms a demand (degree of strictness) on its output into a demand on its arguments. Solutions to this problem in its full generality require large domains and appear both complex and expensive to implement. However, only two kinds of demands arise naturally in lazy normalization of terms, viz., e-demand (normal form needed) and d-demand (root stable or head normal form needed). Based on this observation, we identify three useful forms of strictness for non-flat domains - ee, dd and de. Each of these three forms of strictness play an important role in evaluation of functional programs. Specifically, ee strictness is used for transforming call-by-need to call-by-value and dd strictness is useful in repairing violations of strong sequentiality of equational programs as well as in a critical optimization step used in rewriting implementations of such languages. We present intuitively simple methods to compute them. Our methods are computationally efficient as they are based on small domains (1 point for ee and dd and 2 points for de). They are powerful enough to extract all useful strictness information in practice and are general enough to handle functions defined by rewrite rules. We are able to reason about all user defined data types within a single framework and also handle polymorphism. R. Sekar 0001, Shaunak Pawagi, I. V. Ramakrishnan |
POPL | 1 |
| 1989 | Transforming Strongly Sequential Rewrite Systems with Constructors for Efficient parallel Execution
R. Sekar 0001, Shaunak Pawagi, I. V. Ramakrishnan |
RTA | 1 |