Skip to Main Content Area
CPS-VO
Contact Support
Browse
Calendar
Announcements
Repositories
Groups
Search
Search for Content
Search for a Group
Search for People
Search for a Project
Tagcloud
› Go to login screen
Not a member?
Click here to register!
Forgot username or password?
Cyber-Physical Systems Virtual Organization
Read-only archive of site from September 29, 2023.
CPS-VO
program verification
biblio
Using Safety Properties to Generate Vulnerability Patches
Submitted by aekwall on Mon, 04/20/2020 - 10:45am
relational databases
vulnerability-specific safety properties
source code patches
Software-Vulnerability
Software-Patch
safety-property
safety property
property-based APR
Program-Analysis
Buffer storage
automatic program repair methods
Automated-Program-Repair
relational database security
program debugging
Engines
Safety
program verification
program diagnostics
software maintenance
security vulnerabilities
Libraries
tools
Metrics
composability
pubcrawl
Human behavior
Resiliency
Software
security
security of data
biblio
Scalable Translation Validation of Unverified Legacy OS Code
Submitted by aekwall on Mon, 03/16/2020 - 10:39am
scalable verification
operating systems (computers)
Predictive Metrics
program verification
pubcrawl
PVS7 theorem prover
radare2 reverse engineering tool
Resiliency
reverse engineering
Scalability
operating systems
security
Semantics
specification languages
Theorem Proving
tools
translation validation
unverified legacy OS code
XML
Formal Specification
Metrics
composability
ARM instructions
ARM machines
ARM specification language
ARMv8 ISA
cognition
Compositionality
formal reasoning
Linux Operating System Security
formal validation
formal verification
functional security properties
Google Zircon
large-scale production operating system
Linux
Linux OS
multiple high-level source languages
biblio
Parallel Verification of Software Architecture Design
Submitted by aekwall on Mon, 03/16/2020 - 10:39am
object-oriented programming
software architecture verification
software architecture design
parallel verification
multithreaded environment
multi-threading
monolithic architecture
large-scale complex software systems
component-based software system
Component-Based Software
Circular Dependency
Bottleneck
scalable verification
computer architecture
Compositionality
Predictive Metrics
Scalability
program verification
model checking
Software Architecture
Unified modeling language
Software systems
Production
pubcrawl
Resiliency
biblio
A Systematic Review of the Third Party Auditing in Cloud Security: Security Analysis, Computation Overhead and Performance Evaluation
Submitted by aekwall on Mon, 03/09/2020 - 11:05am
computational overhead
Security Audits
TPA methods
third party auditing method
Third Party Auditing
systematic review
public auditing
Merkel hash tree method
Merkel hash tree
data integrity checking method
considerable efficiency
computation overhead
communication cost
storage management
security of data
Scalability
Cloud Security
performance evaluation
program verification
Security analysis
privacy
pubcrawl
Human behavior
Resiliency
data integrity
cloud storage
Data Security
Cloud Computing
biblio
Formal Security Verification of Concurrent Firmware in SoCs Using Instruction-Level Abstraction for Hardware*
Submitted by grigby1 on Tue, 12/17/2019 - 12:21pm
resilience
Metrics
microprocessor chips
Microprogramming
multi-threading
multithreaded program verification problem
Predictive Metrics
program verification
pubcrawl
intellectual property security
Resiliency
Secure Boot design
security of data
SoC security verification
software verification techniques
system-on-chip
Systems-on-Chip
cyber-physical systems
architecture level
bit-precise reasoning
cognition
composability
Concurrency
concurrency (computers)
concurrent firmware
cyber-physical system
Access Control
firmware
firmware-visible behavior
formal security verification
Frequency modulation
Hardware
Instruction-Level Abstraction
intellectual property blocks
biblio
Formally Verified Cryptographic Web Applications in WebAssembly
Submitted by aekwall on Mon, 12/02/2019 - 12:08pm
verification
Protocols
pubcrawl
public domain software
Resiliency
Scalability
security-critical software
Servers
Signal
sophisticated custom cryptographic components
standard protocols
standards
toolchain
program verification
verification techniques
verification-oriented programming languages
verified cryptographic Web applications
verified HACL cryptographic library
verified implementation
verified-software
web-security
Webassembly
WebAssembly compilers
WebAssembly version
whatsapp
formal verification
Browsers
CoMP
compilation pipeline
compiler
compiler security
Compositionality
cryptographic code
Cryptographic Protocols
cryptographic-library
cryptographic-protocol-verification
Cryptography
authoring languages
high-assurance cryptographic libraries
high-profile attacks
instruction set
Java
JavaScript runtimes
Libraries
low-level subset
Metrics
modern Web applications
program compilers
program diagnostics
biblio
Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation
Submitted by aekwall on Mon, 12/02/2019 - 12:08pm
robust preservation
hyperproperties
linked adversarial code
linked adversarial target code
linked source code
linked target code
liveness
low-level target language
multiple programs
noninterference
property classes
relational hyperproperties
relational properties
good programming languages
robust property preservation
secure compilation
secure compilation chain
Secure interoperability
secure linking
Security Foundations
source language
source-level abstraction
strictly stronger security guarantees
supported security goals
trace properties
compiler security
Compositionality
security of data
Scalability
Resiliency
pubcrawl
Cryptography
Metrics
Libraries
program diagnostics
program verification
Writing
Space exploration
Security Properties
Safety
program compilers
secure code
source program
adversarial contexts
arbitrary adversarial contexts
compiled program
Computer languages
equivalent property-free
formal secure compilation criteria
full abstraction
fully abstract compilation chain
biblio
Information-Flow Preservation in Compiler Optimisations
Submitted by aekwall on Mon, 12/02/2019 - 12:07pm
Scalability
optimization
passive side-channel attacks
program optimisations
Program processors
program transformations
program verification
pubcrawl
Resiliency
optimising compilers
Semantics
side-channel
side-channel attacks
source program
standard compiler passes
standards
target program
I-O Systems
Micromechanical devices
Metrics
information-flow preserving program transformation
information-flow preservation
information-flow leaks
Information Flow
IFP
correct compilers
Compositionality
compiler security
compiler optimisations
compiler
CompCert C compiler
security
i-o systems security
biblio
What You Get is What You C: Controlling Side Effects in Mainstream C Compilers
Submitted by aekwall on Mon, 12/02/2019 - 12:07pm
language security
compiler performance
compiler upgrade
compiler writers
compilers
constant-time
CPUs
crypto code
cryptographic algorithm
cryptographic protocol security
erasing
implicit properties
compiler optimizations
LLVM
mainstream C compilers
secure code
Security Engineers
side channels
side effects
stack
timing channel
zeroing
compiler security
timing
Cryptography
Cryptographic Protocols
Program processors
Resiliency
pubcrawl
Metrics
standards
optimization
Libraries
optimisation
program verification
Scalability
Security Properties
Compositionality
program compilers
C
C abstract machine
C++ language
careful programmer
Clang
compiler commands
Compiler Optimization
biblio
Deductive Verification of Distributed Protocols in First-Order Logic
Submitted by grigby1 on Tue, 11/12/2019 - 4:30pm
infinite-state systems
verification problem
validity checking
Tutorials
tools
Theorem Proving
SMT solvers
Safety
pubcrawl
Protocols
protocol verification
program verification
privacy
policy-based governance
long standing research goal
logical verification conditions
automated provers
formal verification
Formal Specification
formal logic
first-order logic
distributed systems
distributed protocols
design automation
deductive verification approach
Computer languages
Compositionality
composability
complex systems
collaboration
cognition
automated theorem provers
« first
‹ previous
1
2
3
4
next ›
last »
