From 675caad0ac7b86e1135fbe20d51f327e5a3a6c35 Mon Sep 17 00:00:00 2001 From: Peter Rugg Date: Tue, 14 Jul 2020 15:34:38 +0100 Subject: [PATCH 1/9] Trap for permission failures on mem access --- .../procs/RV64G_OOO/MemExePipeline.bsv | 4 +-- src_Core/RISCY_OOO/procs/lib/Decode.bsv | 4 --- src_Core/RISCY_OOO/procs/lib/Exec.bsv | 34 +++++++++++++++++-- 3 files changed, 33 insertions(+), 9 deletions(-) diff --git a/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv b/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv index 073a1fd..aba8ed8 100644 --- a/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv +++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv @@ -446,7 +446,7 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); if(x.regs.src1 matches tagged Valid .src1 &&& src1 != 0) begin rVal1 <- readRFBypass(src1, regsReady.src1, inIfc.rf_rd1(src1), bypassWire); end - if (x.ddc_offset) rVal1 = nullWithAddr(getAddr(rVal1) + getAddr(ddc)); + if (x.ddc_offset) rVal1 = incOffset(ddc, getAddr(rVal1)).value; // get rVal2 (check bypass) CapPipe rVal2 = nullCap; @@ -522,7 +522,7 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); store_data_BE: origBE, `endif misaligned: memAddrMisaligned(getAddr(vaddr), origBE), - capException: capChecks(x.rVal1, x.rVal2, ddc, x.cap_checks, ?), + capException: capChecksMem(x.rVal1, x.rVal2, x.cap_checks, x.mem_func, origBE), check: prepareBoundsCheck(x.rVal1, x.rVal2, almightyCap/*ToDo: pcc*/, ddc, getAddr(vaddr), pack(countOnes(pack(origBE))), x.cap_checks) }, diff --git a/src_Core/RISCY_OOO/procs/lib/Decode.bsv b/src_Core/RISCY_OOO/procs/lib/Decode.bsv index 597e2e2..fb64d60 100755 --- a/src_Core/RISCY_OOO/procs/lib/Decode.bsv +++ b/src_Core/RISCY_OOO/procs/lib/Decode.bsv @@ -257,12 +257,8 @@ function CapChecks memCapChecks(Bool cap_mode); capChecks.check_inclusive = True; if (cap_mode) begin capChecks.check_authority_src = Src1; - capChecks.src1_tag = True; - capChecks.src1_unsealed = True; end else begin capChecks.check_authority_src = Ddc; - capChecks.ddc_tag = True; - capChecks.ddc_unsealed = True; end return capChecks; endfunction diff --git a/src_Core/RISCY_OOO/procs/lib/Exec.bsv b/src_Core/RISCY_OOO/procs/lib/Exec.bsv index 64a63e5..63aa78f 100755 --- a/src_Core/RISCY_OOO/procs/lib/Exec.bsv +++ b/src_Core/RISCY_OOO/procs/lib/Exec.bsv @@ -45,10 +45,10 @@ import CHERICC_Fat::*; import ISA_Decls_CHERI::*; (* noinline *) -function Maybe#(CSR_XCapCause) capChecks(CapPipe a, CapPipe b, CapPipe ddc, CapChecks toCheck, Bool cap_exact); +function Maybe#(CSR_XCapCause) capChecksExec(CapPipe a, CapPipe b, CapPipe ddc, CapChecks toCheck, Bool cap_exact); function Maybe#(CSR_XCapCause) e1(CHERIException e) = Valid(CSR_XCapCause{cheri_exc_reg: toCheck.rn1, cheri_exc_code: e}); function Maybe#(CSR_XCapCause) e2(CHERIException e) = Valid(CSR_XCapCause{cheri_exc_reg: toCheck.rn2, cheri_exc_code: e}); - function Maybe#(CSR_XCapCause) eDDC(CHERIException e) = Valid(CSR_XCapCause{cheri_exc_reg: 6'b100001, cheri_exc_code: e}); // Not sure where the proper reg number of DDC is stored... + function Maybe#(CSR_XCapCause) eDDC(CHERIException e) = Valid(CSR_XCapCause{cheri_exc_reg: {1'b1, pack(SCR_DDC)}, cheri_exc_code: e}); Maybe#(CSR_XCapCause) result = Invalid; if (toCheck.ddc_tag && !isValidCap(ddc)) result = eDDC(TagViolation); @@ -99,6 +99,34 @@ function Maybe#(CSR_XCapCause) capChecks(CapPipe a, CapPipe b, CapPipe ddc, CapC return result; endfunction +(* noinline *) +function Maybe#(CSR_XCapCause) capChecksMem(CapPipe auth, CapPipe data, CapChecks toCheck, MemFunc mem_func, MemDataByteEn byteEn); + function Maybe#(CSR_XCapCause) eAuth(CHERIException e) = Valid(CSR_XCapCause{cheri_exc_reg: case (toCheck.check_authority_src) matches Src1: toCheck.rn1; + Ddc: {1'b1, pack(SCR_DDC)}; + endcase + , cheri_exc_code: e}); + Maybe#(CSR_XCapCause) result = Invalid; + if (!isValidCap(auth)) + result = eAuth(TagViolation); + else if (getKind(auth) != UNSEALED) + result = eAuth(SealViolation); + else if (mem_func == Ld || mem_func == Lr || mem_func == Amo) begin + if (!getHardPerms(auth).permitLoad) + result = eAuth(PermitRViolation); + end + else if (mem_func == St || mem_func == Sc || mem_func == Amo) begin + if (!getHardPerms(auth).permitStore) + result = eAuth(PermitWViolation); + if (isValidCap(data) && byteEn == replicate(True)) begin + if (!getHardPerms(auth).permitStoreCap) + result = eAuth(PermitWCapViolation); + if (!getHardPerms(auth).permitStoreLocalCap && getHardPerms(data).global) + result = eAuth(PermitWLocalCapViolation); + end + end + return result; +endfunction + (* noinline *) function Maybe#(BoundsCheck) prepareBoundsCheck(CapPipe a, CapPipe b, CapPipe pcc, CapPipe ddc, Data vaddr, Bit#(5) size, // These two are only used in the memory pipe. May factor into two functions later. @@ -380,7 +408,7 @@ function ExecResult basicExec(DecodedInst dInst, CapPipe rVal1, CapPipe rVal2, C if (!cf.taken) dInst.capChecks.check_enable = False; end - Maybe#(CSR_XCapCause) capException = capChecks(rVal1, aluVal2, nullCap, dInst.capChecks, cap_exact); + Maybe#(CSR_XCapCause) capException = capChecksExec(rVal1, aluVal2, nullCap, dInst.capChecks, cap_exact); Maybe#(BoundsCheck) boundsCheck = prepareBoundsCheck(rVal1, aluVal2, pcc, nullCap, 0, 0, // These three are only used in the memory pipe dInst.capChecks); From b44a912756b6b6d39399e5318d49337919295efb Mon Sep 17 00:00:00 2001 From: Peter Rugg Date: Tue, 14 Jul 2020 22:41:51 +0100 Subject: [PATCH 2/9] Don't require ASR to read PCC The dInst.scr field was accidentally left populated in this case, causing the check to occur --- src_Core/RISCY_OOO/procs/lib/Decode.bsv | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src_Core/RISCY_OOO/procs/lib/Decode.bsv b/src_Core/RISCY_OOO/procs/lib/Decode.bsv index fb64d60..81fbf94 100755 --- a/src_Core/RISCY_OOO/procs/lib/Decode.bsv +++ b/src_Core/RISCY_OOO/procs/lib/Decode.bsv @@ -954,7 +954,8 @@ function DecodeResult decode(Instruction inst, Bool cap_mode); dInst.iType = rs1 == 0 ? Cap : Scr; regs.dst = Valid(tagged Gpr rd); regs.src1 = Valid(tagged Gpr rs1); - dInst.scr = Valid (unpackSCR(rs2)); + + let scr = unpackSCR(rs2); let scrType = case (rs2[1:0]) 0: TCC; @@ -963,12 +964,14 @@ function DecodeResult decode(Instruction inst, Bool cap_mode); endcase; // Decode SCR read to PCC as AUIPCC 0 - if (dInst.scr.Valid == SCR_PCC) begin + if (scr == SCR_PCC) begin dInst.iType = Auipcc; dInst.execFunc = tagged Alu Add; regs.src1 = Invalid; dInst.csr = tagged Invalid; dInst.capChecks.scr_read_only = True; + end else begin + dInst.scr = Valid (scr); end dInst.capFunc = CapModify (SpecialRW (scrType)); From a74596c9568e81eff38f0c58359e16954625c6eb Mon Sep 17 00:00:00 2001 From: Peter Rugg Date: Thu, 16 Jul 2020 14:06:26 +0100 Subject: [PATCH 3/9] Fix CCall being impossible The cap to be checked (rs1) was being overwritten with the unsealed jump target before the type was checked --- src_Core/RISCY_OOO/procs/lib/Exec.bsv | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src_Core/RISCY_OOO/procs/lib/Exec.bsv b/src_Core/RISCY_OOO/procs/lib/Exec.bsv index 63aa78f..779829a 100755 --- a/src_Core/RISCY_OOO/procs/lib/Exec.bsv +++ b/src_Core/RISCY_OOO/procs/lib/Exec.bsv @@ -403,12 +403,12 @@ function ExecResult basicExec(DecodedInst dInst, CapPipe rVal1, CapPipe rVal2, C BrFunc br_f = dInst.execFunc matches tagged Br .br_f ? br_f : NT; cf.taken = aluBr(getAddr(rVal1), getAddr(rVal2), br_f); cf.nextPc = brAddrCalc(pcc, rVal1, dInst.iType, fromMaybe(0,getDInstImm(dInst)), cf.taken, orig_inst, newPcc); + + Maybe#(CSR_XCapCause) capException = capChecksExec(rVal1, aluVal2, nullCap, dInst.capChecks, cap_exact); if (dInst.execFunc matches tagged Br .unused) begin rVal1 = cf.nextPc; if (!cf.taken) dInst.capChecks.check_enable = False; end - - Maybe#(CSR_XCapCause) capException = capChecksExec(rVal1, aluVal2, nullCap, dInst.capChecks, cap_exact); Maybe#(BoundsCheck) boundsCheck = prepareBoundsCheck(rVal1, aluVal2, pcc, nullCap, 0, 0, // These three are only used in the memory pipe dInst.capChecks); From 0040b05ada856a2697bae6c980058b9c3e1c8242 Mon Sep 17 00:00:00 2001 From: Peter Rugg Date: Tue, 21 Jul 2020 16:02:37 +0100 Subject: [PATCH 4/9] Add page table cap store checking --- .../procs/RV64G_OOO/MemExePipeline.bsv | 5 +- src_Core/RISCY_OOO/procs/lib/DTlb.bsv | 30 +++++++----- src_Core/RISCY_OOO/procs/lib/ITlb.bsv | 8 ++- src_Core/RISCY_OOO/procs/lib/L2Tlb.bsv | 1 + src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv | 2 + src_Core/RISCY_OOO/procs/lib/TlbTypes.bsv | 49 ++++++++++++++----- 6 files changed, 69 insertions(+), 26 deletions(-) diff --git a/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv b/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv index aba8ed8..1318f6f 100644 --- a/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv +++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv @@ -108,6 +108,7 @@ typedef struct { ByteEn store_data_BE; `endif Bool misaligned; + Bool capStore; Maybe#(CSR_XCapCause) capException; Maybe#(BoundsCheck) check; } MemExeToFinish deriving(Bits, FShow); @@ -158,7 +159,8 @@ module mkDTlbSynth(DTlbSynth); write: (case(x.mem_func) St, Sc, Amo: True; default: False; - endcase) + endcase), + cap: x.capStore }; endfunction let m <- mkDTlb(getTlbReq); @@ -522,6 +524,7 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); store_data_BE: origBE, `endif misaligned: memAddrMisaligned(getAddr(vaddr), origBE), + capStore: isValidCap(data) && pack(origBE) == ~0, capException: capChecksMem(x.rVal1, x.rVal2, x.cap_checks, x.mem_func, origBE), check: prepareBoundsCheck(x.rVal1, x.rVal2, almightyCap/*ToDo: pcc*/, ddc, getAddr(vaddr), pack(countOnes(pack(origBE))), x.cap_checks) diff --git a/src_Core/RISCY_OOO/procs/lib/DTlb.bsv b/src_Core/RISCY_OOO/procs/lib/DTlb.bsv index c0eedf9..6d59bc7 100644 --- a/src_Core/RISCY_OOO/procs/lib/DTlb.bsv +++ b/src_Core/RISCY_OOO/procs/lib/DTlb.bsv @@ -271,11 +271,14 @@ module mkDTlb#( end else if(pRs.entry matches tagged Valid .en) begin // check permission - if(hasVMPermission(vm_info, - en.pteType, - en.ppn, - en.level, - r.write ? DataStore : DataLoad)) begin + let permCheck = hasVMPermission(vm_info, + en.pteType, + en.pteUpperType, + en.ppn, + en.level, + r.write ? DataStore : DataLoad, + r.cap); + if (permCheck.allowed) begin // fill TLB, and record resp tlb.addEntry(en); let trans_addr = translate(r.addr, en.ppn, en.level); @@ -287,7 +290,7 @@ module mkDTlb#( end else begin // page fault - Exception fault = r.write ? StorePageFault : LoadPageFault; + Exception fault = permCheck.excCode; pendResp[idx] <= tuple2(?, Valid (fault)); if(verbose) begin $display("[DTLB] refill no permission: idx %d; ", idx, fshow(r)); @@ -448,11 +451,14 @@ module mkDTlb#( // TLB hit let entry = trans_result.entry; // check permission - if (hasVMPermission(vm_info, - entry.pteType, - entry.ppn, - entry.level, - r.write ? DataStore : DataLoad)) begin + let permCheck = hasVMPermission(vm_info, + entry.pteType, + entry.pteUpperType, + entry.ppn, + entry.level, + r.write ? DataStore : DataLoad, + r.cap); + if (permCheck.allowed) begin // update TLB replacement info tlb.updateRepByHit(trans_result.index); // translate addr @@ -472,7 +478,7 @@ module mkDTlb#( end else begin // page fault - Exception fault = r.write ? StorePageFault : LoadPageFault; + Exception fault = permCheck.excCode; pendWait[idx] <= None; pendResp[idx] <= tuple2(?, Valid (fault)); if(verbose) $display("[DTLB] req no permission: idx %d; ", idx, fshow(r)); diff --git a/src_Core/RISCY_OOO/procs/lib/ITlb.bsv b/src_Core/RISCY_OOO/procs/lib/ITlb.bsv index 485044f..da25e62 100644 --- a/src_Core/RISCY_OOO/procs/lib/ITlb.bsv +++ b/src_Core/RISCY_OOO/procs/lib/ITlb.bsv @@ -176,9 +176,11 @@ module mkITlb(ITlb::ITlb); // check permission if(hasVMPermission(vm_info, en.pteType, + en.pteUpperType, en.ppn, en.level, - InstFetch)) begin + InstFetch, + False).allowed) begin // fill TLB and resp to proc tlb.addEntry(en); let trans_addr = translate(vaddr, en.ppn, en.level); @@ -285,9 +287,11 @@ module mkITlb(ITlb::ITlb); // check permission if(hasVMPermission(vm_info, entry.pteType, + entry.pteUpperType, entry.ppn, entry.level, - InstFetch)) begin + InstFetch, + False).allowed) begin // update replacement info tlb.updateRepByHit(trans_result.index); // translate addr diff --git a/src_Core/RISCY_OOO/procs/lib/L2Tlb.bsv b/src_Core/RISCY_OOO/procs/lib/L2Tlb.bsv index ab8b58e..139169f 100644 --- a/src_Core/RISCY_OOO/procs/lib/L2Tlb.bsv +++ b/src_Core/RISCY_OOO/procs/lib/L2Tlb.bsv @@ -653,6 +653,7 @@ module mkL2Tlb(L2Tlb::L2Tlb); vpn: masked_vpn, ppn: masked_ppn, pteType: pte.pteType, + pteUpperType: pte.pteUpperType, level: walkLevel, asid: vm_info.asid }; diff --git a/src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv b/src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv index c64bb22..00cf212 100755 --- a/src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv +++ b/src_Core/RISCY_OOO/procs/lib/ProcTypes.bsv @@ -393,6 +393,8 @@ typedef enum { InstPageFault = 5'd12, LoadPageFault = 5'd13, StorePageFault = 5'd15, + LoadCapPageFault = 5'd26, + StoreCapPageFault = 5'd27, CHERIFault = 5'd28 } Exception deriving(Bits, Eq, FShow); diff --git a/src_Core/RISCY_OOO/procs/lib/TlbTypes.bsv b/src_Core/RISCY_OOO/procs/lib/TlbTypes.bsv index 41f4eda..b30a2a0 100644 --- a/src_Core/RISCY_OOO/procs/lib/TlbTypes.bsv +++ b/src_Core/RISCY_OOO/procs/lib/TlbTypes.bsv @@ -31,6 +31,7 @@ import ProcTypes::*; typedef struct{ Addr addr; Bool write; + Bool cap; } TlbReq deriving(Eq, Bits, FShow); typedef Tuple2#(Addr, Maybe#(Exception)) TlbResp; @@ -66,7 +67,13 @@ typedef struct { } PTEType deriving (Bits, Eq, FShow); typedef struct { - Bit#(10) reserved; + Bool cap_writable; + Bool cap_readable; +} PTEUpperType deriving (Bits, Eq, FShow); + +typedef struct { + PTEUpperType pteUpperType; + Bit#(8) reserved; Ppn ppn; Bit#(2) reserved_sw; // reserved for supervisor software PTEType pteType; @@ -78,6 +85,7 @@ typedef struct { Vpn vpn; Ppn ppn; PTEType pteType; + PTEUpperType pteUpperType; PageWalkLevel level; Asid asid; } TlbEntry deriving (Bits, Eq, FShow); @@ -169,10 +177,16 @@ typedef enum { DataStore // also contain DataLoad } TlbAccessType deriving(Bits, Eq, FShow); -function Bool hasVMPermission( +typedef struct { + Bool allowed; + Exception excCode; // Only defined if !allowed +} TlbPermissionCheck deriving(Bits, Eq, FShow); + +function TlbPermissionCheck hasVMPermission( VMInfo vm_info, - PTEType pte_type, Ppn ppn, PageWalkLevel level, - TlbAccessType access + PTEType pte_type, PTEUpperType pte_upper_type, + Ppn ppn, PageWalkLevel level, + TlbAccessType access, Bool cap ); // try to find any page fault Bool fault = False; @@ -229,13 +243,26 @@ function Bool hasVMPermission( end endcase - // check if accessed or dirty bit needs to be set - if(!pte_type.accessed) begin - fault = True; - end - if(access == DataStore && !pte_type.dirty) begin - fault = True; + TlbPermissionCheck ret = TlbPermissionCheck { + allowed: !fault, + excCode: access == DataStore ? StorePageFault : LoadPageFault}; + + if (!fault) begin + if (cap && access == DataStore && !pte_upper_type.cap_writable) begin + ret.allowed = False; + ret.excCode = StoreCapPageFault; + end else begin + // check if accessed or dirty bit needs to be set + if(!pte_type.accessed) begin + ret.allowed = False; + ret.excCode = access == DataStore ? StorePageFault : LoadPageFault; + end + if(access == DataStore && !pte_type.dirty) begin + ret.allowed = False; + ret.excCode = access == DataStore ? StorePageFault : LoadPageFault; + end + end end - return !fault; + return ret; endfunction From c693462f6b5a331c9108dc88e3e4c6fabc2ffd43 Mon Sep 17 00:00:00 2001 From: Peter Rugg Date: Wed, 22 Jul 2020 15:54:49 +0100 Subject: [PATCH 5/9] Add tag-clearing due to cap load perm and PTE bits --- .../RISCY_OOO/procs/RV64G_OOO/FetchStage.bsv | 2 +- .../procs/RV64G_OOO/MemExePipeline.bsv | 26 ++++++++++++++----- .../RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv | 2 +- src_Core/RISCY_OOO/procs/lib/DTlb.bsv | 15 ++++++----- src_Core/RISCY_OOO/procs/lib/ITlb.bsv | 12 ++++----- src_Core/RISCY_OOO/procs/lib/SplitLSQ.bsv | 13 ++++++++-- src_Core/RISCY_OOO/procs/lib/TlbTypes.bsv | 8 +++--- 7 files changed, 51 insertions(+), 27 deletions(-) diff --git a/src_Core/RISCY_OOO/procs/RV64G_OOO/FetchStage.bsv b/src_Core/RISCY_OOO/procs/RV64G_OOO/FetchStage.bsv index 6a0c41f..58b665a 100644 --- a/src_Core/RISCY_OOO/procs/RV64G_OOO/FetchStage.bsv +++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/FetchStage.bsv @@ -616,7 +616,7 @@ module mkFetchStage(FetchStage); f12f2.deq; // Get TLB response - match {.phys_pc, .cause} <- tlb_server.response.get; + match {.phys_pc, .cause, .allow_cap} <- tlb_server.response.get; // Access main mem or boot rom if no TLB exception Bool access_mmio = False; diff --git a/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv b/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv index 1318f6f..df266a2 100644 --- a/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv +++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv @@ -109,6 +109,7 @@ typedef struct { `endif Bool misaligned; Bool capStore; + Bool allowCap; Maybe#(CSR_XCapCause) capException; Maybe#(BoundsCheck) check; } MemExeToFinish deriving(Bits, FShow); @@ -525,6 +526,7 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); `endif misaligned: memAddrMisaligned(getAddr(vaddr), origBE), capStore: isValidCap(data) && pack(origBE) == ~0, + allowCap: getHardPerms(x.rVal1).permitLoadCap, capException: capChecksMem(x.rVal1, x.rVal2, x.cap_checks, x.mem_func, origBE), check: prepareBoundsCheck(x.rVal1, x.rVal2, almightyCap/*ToDo: pcc*/, ddc, getAddr(vaddr), pack(countOnes(pack(origBE))), x.cap_checks) @@ -537,7 +539,7 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); dTlb.deqProcResp; let dTlbResp = dTlb.procResp; let x = dTlbResp.inst; - let {paddr, expCause} = dTlbResp.resp; + let {paddr, expCause, allowCapPTE} = dTlbResp.resp; Maybe#(Trap) cause = Invalid; if (expCause matches tagged Valid .c) cause = Valid(Exception(c)); @@ -618,7 +620,7 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); // update LSQ LSQUpdateAddrResult updRes <- lsq.updateAddr( - x.ldstq_tag, cause, paddr, isMMIO, x.shiftedBE + x.ldstq_tag, cause, x.allowCap && allowCapPTE, paddr, isMMIO, x.shiftedBE ); // issue non-MMIO Ld which has no exception and is not waiting for @@ -743,7 +745,9 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); LSQRespLdResult res <- lsq.respLd(tag, data); if(verbose) $display("%t : ", $time, rule_name, " ", fshow(tag), "; ", fshow(data), "; ", fshow(res)); if(res.dst matches tagged Valid .dst) begin - inIfc.writeRegFile(dst.indx, fromMem(unpack(pack(res.data)))); + CapPipe dataUnpacked = fromMem(unpack(pack(res.data))); + dataUnpacked = setValidCap(dataUnpacked, res.allowCap && isValidCap(dataUnpacked)); + inIfc.writeRegFile(dst.indx, dataUnpacked); `ifdef INCLUDE_TANDEM_VERIF inIfc.rob_setExecuted_doFinishMem_RegData (res.instTag, res.data); @@ -906,7 +910,9 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); MemTaggedData resp = gatherLoad(lsqDeqLd.paddr, lsqDeqLd.byteEn, lsqDeqLd.unsignedLd, d); // write reg file & set ROB as Executed & wakeup rs if(lsqDeqLd.dst matches tagged Valid .dst) begin - inIfc.writeRegFile(dst.indx, fromMem(unpack(pack(resp)))); + CapPipe dataUnpacked = fromMem(unpack(pack(resp))); + dataUnpacked = setValidCap(dataUnpacked, lsqDeqLd.allowCap && isValidCap(dataUnpacked)); + inIfc.writeRegFile(dst.indx, dataUnpacked); inIfc.setRegReadyAggr_mem(dst.indx); `ifdef INCLUDE_TANDEM_VERIF inIfc.rob_setExecuted_doFinishMem_RegData (lsqDeqLd.instTag, resp); @@ -994,7 +1000,9 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); MemTaggedData resp = gatherLoad(lsqDeqLd.paddr, lsqDeqLd.byteEn, lsqDeqLd.unsignedLd, d); // write reg file & wakeup rs (this wakeup is late but MMIO is rare) & set ROB as Executed if(lsqDeqLd.dst matches tagged Valid .dst) begin - inIfc.writeRegFile(dst.indx, fromMem(tuple2(resp.tag,unpack(pack(resp.data))))); + CapPipe dataUnpacked = fromMem(tuple2(resp.tag,unpack(pack(resp.data)))); + dataUnpacked = setValidCap(dataUnpacked, lsqDeqLd.allowCap && isValidCap(dataUnpacked)); + inIfc.writeRegFile(dst.indx, dataUnpacked); inIfc.setRegReadyAggr_mem(dst.indx); `ifdef INCLUDE_TANDEM_VERIF inIfc.rob_setExecuted_doFinishMem_RegData (lsqDeqLd.instTag, resp); @@ -1247,7 +1255,9 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); MemTaggedData resp <- toGet(respLrScAmoQ).get; // write reg file & set ROB as Executed & wake up rs if(lsqDeqSt.dst matches tagged Valid .dst) begin - inIfc.writeRegFile(dst.indx, fromMem(tuple2(resp.tag, pack(resp.data)))); + CapPipe dataUnpacked = fromMem(tuple2(resp.tag, pack(resp.data))); + dataUnpacked = setValidCap(dataUnpacked, False); // TODO no allowCap around. Can a cap be loaded this way (e.g. AMOSWAP?) + inIfc.writeRegFile(dst.indx, dataUnpacked); inIfc.setRegReadyAggr_mem(dst.indx); `ifdef INCLUDE_TANDEM_VERIF inIfc.rob_setExecuted_doFinishMem_RegData (lsqDeqSt.instTag, resp); @@ -1353,7 +1363,9 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline); MemTaggedData resp = inIfc.mmioRespVal.data; // write reg file & wakeup rs (this wakeup is late but MMIO is rare) & set ROB as Executed if(lsqDeqSt.dst matches tagged Valid .dst) begin - inIfc.writeRegFile(dst.indx, fromMem(tuple2(resp.tag, pack(resp.data)))); + CapPipe dataUnpacked = fromMem(tuple2(resp.tag, pack(resp.data))); + dataUnpacked = setValidCap(dataUnpacked, False); // TODO no allowCap around. Can a cap be loaded this way (e.g. AMOSWAP?) + inIfc.writeRegFile(dst.indx, dataUnpacked); inIfc.setRegReadyAggr_mem(dst.indx); `ifdef INCLUDE_TANDEM_VERIF inIfc.rob_setExecuted_doFinishMem_RegData (lsqDeqSt.instTag, resp); diff --git a/src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv b/src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv index 7657142..6c7cf77 100644 --- a/src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv +++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv @@ -704,7 +704,7 @@ module mkRenameStage#(RenameInput inIfc)(RenameStage); "Mem (non-Fence) needs imm for virtual addr"); // put in ldstq if(isLdQ) begin - lsq.enqLd(inst_tag, mem_inst, phy_regs.dst, spec_bits); + lsq.enqLd(inst_tag, mem_inst, allow_cap, phy_regs.dst, spec_bits); end else begin lsq.enqSt(inst_tag, mem_inst, phy_regs.dst, spec_bits); diff --git a/src_Core/RISCY_OOO/procs/lib/DTlb.bsv b/src_Core/RISCY_OOO/procs/lib/DTlb.bsv index 6d59bc7..28fe5e6 100644 --- a/src_Core/RISCY_OOO/procs/lib/DTlb.bsv +++ b/src_Core/RISCY_OOO/procs/lib/DTlb.bsv @@ -282,7 +282,7 @@ module mkDTlb#( // fill TLB, and record resp tlb.addEntry(en); let trans_addr = translate(r.addr, en.ppn, en.level); - pendResp[idx] <= tuple2(trans_addr, Invalid); + pendResp[idx] <= tuple3(trans_addr, Invalid, permCheck.allowCap); if(verbose) begin $display("[DTLB] refill: idx %d; ", idx, fshow(r), "; ", fshow(trans_addr)); @@ -291,7 +291,7 @@ module mkDTlb#( else begin // page fault Exception fault = permCheck.excCode; - pendResp[idx] <= tuple2(?, Valid (fault)); + pendResp[idx] <= tuple3(?, Valid (fault), False); if(verbose) begin $display("[DTLB] refill no permission: idx %d; ", idx, fshow(r)); end @@ -300,7 +300,7 @@ module mkDTlb#( else begin // page fault Exception fault = r.write ? StorePageFault : LoadPageFault; - pendResp[idx] <= tuple2(?, Valid (fault)); + pendResp[idx] <= tuple3(?, Valid (fault), False); if(verbose) $display("[DTLB] refill page fault: idx %d; ", idx, fshow(r)); end @@ -436,7 +436,7 @@ module mkDTlb#( // (Because we are always non speculative in M mode) if (!vm_info.sanctum_authShared && outOfProtectionDomain(vm_info, r.addr))begin pendWait[idx] <= None; - pendResp[idx] <= tuple2(?, Valid (LoadAccessFault)); + pendResp[idx] <= tuple3(?, Valid (LoadAccessFault), False); end `else // No security check @@ -458,13 +458,14 @@ module mkDTlb#( entry.level, r.write ? DataStore : DataLoad, r.cap); + $display("Permission check output 2: ", fshow(permCheck)); if (permCheck.allowed) begin // update TLB replacement info tlb.updateRepByHit(trans_result.index); // translate addr Addr trans_addr = translate(r.addr, entry.ppn, entry.level); pendWait[idx] <= None; - pendResp[idx] <= tuple2(trans_addr, Invalid); + pendResp[idx] <= tuple3(trans_addr, Invalid, permCheck.allowCap); if(verbose) begin $display("[DTLB] req (hit): idx %d; ", idx, fshow(r), "; ", fshow(trans_result)); @@ -480,7 +481,7 @@ module mkDTlb#( // page fault Exception fault = permCheck.excCode; pendWait[idx] <= None; - pendResp[idx] <= tuple2(?, Valid (fault)); + pendResp[idx] <= tuple3(?, Valid (fault), False); if(verbose) $display("[DTLB] req no permission: idx %d; ", idx, fshow(r)); end end @@ -524,7 +525,7 @@ module mkDTlb#( else begin // bare mode pendWait[idx] <= None; - pendResp[idx] <= tuple2(r.addr, Invalid); + pendResp[idx] <= tuple3(r.addr, Invalid, True); if(verbose) $display("DTLB %m req (bare): ", fshow(r)); end diff --git a/src_Core/RISCY_OOO/procs/lib/ITlb.bsv b/src_Core/RISCY_OOO/procs/lib/ITlb.bsv index da25e62..c172ea6 100644 --- a/src_Core/RISCY_OOO/procs/lib/ITlb.bsv +++ b/src_Core/RISCY_OOO/procs/lib/ITlb.bsv @@ -184,7 +184,7 @@ module mkITlb(ITlb::ITlb); // fill TLB and resp to proc tlb.addEntry(en); let trans_addr = translate(vaddr, en.ppn, en.level); - hitQ.enq(tuple2(trans_addr, Invalid)); + hitQ.enq(tuple3(trans_addr, Invalid, False)); if(verbose) begin $display("ITLB %m refill: ", fshow(vaddr), " ; ", fshow(trans_addr)); @@ -192,7 +192,7 @@ module mkITlb(ITlb::ITlb); end else begin // page fault - hitQ.enq(tuple2(?, Valid (InstPageFault))); + hitQ.enq(tuple3(?, Valid (InstPageFault), False)); if(verbose) begin $display("ITLB %m refill no permission: ", fshow(vaddr)); end @@ -200,7 +200,7 @@ module mkITlb(ITlb::ITlb); end else begin // page fault - hitQ.enq(tuple2(?, Valid (InstPageFault))); + hitQ.enq(tuple3(?, Valid (InstPageFault), False)); if(verbose) $display("ITLB %m refill page fault: ", fshow(vaddr)); end // miss resolved @@ -298,7 +298,7 @@ module mkITlb(ITlb::ITlb); Addr trans_addr = translate( vaddr, entry.ppn, entry.level ); - hitQ.enq(tuple2(trans_addr, Invalid)); + hitQ.enq(tuple3(trans_addr, Invalid, False)); if(verbose) begin $display("ITLB %m req (hit): ", fshow(vaddr), " ; ", fshow(trans_result)); @@ -306,7 +306,7 @@ module mkITlb(ITlb::ITlb); end else begin // page fault - hitQ.enq(tuple2(?, Valid (InstPageFault))); + hitQ.enq(tuple3(?, Valid (InstPageFault), False)); if(verbose) begin $display("ITLB %m req no permission: ", fshow(vaddr)); @@ -330,7 +330,7 @@ module mkITlb(ITlb::ITlb); end else begin // bare mode, no translation - hitQ.enq(tuple2(vaddr, Invalid)); + hitQ.enq(tuple3(vaddr, Invalid, False)); if (verbose) $display("ITLB %m req (bare): ", fshow(vaddr)); end diff --git a/src_Core/RISCY_OOO/procs/lib/SplitLSQ.bsv b/src_Core/RISCY_OOO/procs/lib/SplitLSQ.bsv index 25b734f..527721e 100644 --- a/src_Core/RISCY_OOO/procs/lib/SplitLSQ.bsv +++ b/src_Core/RISCY_OOO/procs/lib/SplitLSQ.bsv @@ -294,6 +294,7 @@ typedef struct { typedef struct { Bool wrongPath; Maybe#(PhyDst) dst; + Bool allowCap; `ifdef INCLUDE_TANDEM_VERIF InstTag instTag; // For recording Ld data in ROB `endif @@ -318,6 +319,7 @@ typedef struct { Bool isMMIO; MemDataByteEn shiftedBE; Maybe#(Trap) fault; + Bool allowCap; Maybe#(LdKilledBy) killed; } LdQDeqEntry deriving (Bits, Eq, FShow); @@ -332,6 +334,7 @@ typedef struct { Bool isMMIO; MemDataByteEn shiftedBE; MemTaggedData stData; + Bool allowCap; Maybe#(Trap) fault; } StQDeqEntry deriving (Bits, Eq, FShow); @@ -363,7 +366,7 @@ interface SplitLSQ; method ActionValue#(LSQUpdateAddrResult) updateAddr( LdStQTag lsqTag, Maybe#(Trap) fault, // below are only meaningful wen fault is Invalid - Addr paddr, Bool isMMIO, MemDataByteEn shiftedBE + Bool allowCap, Addr paddr, Bool isMMIO, MemDataByteEn shiftedBE ); // Issue a load, and remove dependence on this load issue. method ActionValue#(LSQIssueLdResult) issueLd( @@ -631,6 +634,7 @@ module mkSplitLSQ(SplitLSQ); Vector#(LdQSize, Reg#(LdQMemFunc)) ld_memFunc <- replicateM(mkRegU); Vector#(LdQSize, Reg#(Bool)) ld_unsigned <- replicateM(mkRegU); Vector#(LdQSize, Reg#(MemDataByteEn)) ld_byteEn <- replicateM(mkRegU); + Vector#(LdQSize, Reg#(Bool)) ld_allowCap <- replicateM(mkRegU); Vector#(LdQSize, Reg#(Bool)) ld_acq <- replicateM(mkRegU); Vector#(LdQSize, Reg#(Bool)) ld_rel <- replicateM(mkRegU); Vector#(LdQSize, Reg#(Maybe#(PhyDst))) ld_dst <- replicateM(mkRegU); @@ -1525,7 +1529,7 @@ module mkSplitLSQ(SplitLSQ); method ActionValue#(LSQUpdateAddrResult) updateAddr( LdStQTag lsqTag, Maybe#(Trap) fault, - Addr pa, Bool mmio, MemDataByteEn shift_be + Bool allowCap, Addr pa, Bool mmio, MemDataByteEn shift_be ); // index vec for vector functions Vector#(LdQSize, LdQTag) idxVec = genWith(fromInteger); @@ -1566,6 +1570,7 @@ module mkSplitLSQ(SplitLSQ); ld_fault_updAddr[tag] <= fault; ld_computed_updAddr[tag] <= !isValid(fault); ld_paddr_updAddr[tag] <= pa; + ld_allowCap[tag] <= allowCap; ld_isMMIO_updAddr[tag] <= mmio; ld_shiftedBE_updAddr[tag] <= shift_be; @@ -1994,6 +1999,7 @@ module mkSplitLSQ(SplitLSQ); let res = LSQRespLdResult { wrongPath: False, dst: Invalid, + allowCap: False, `ifdef INCLUDE_TANDEM_VERIF instTag: ld_instTag [t], // For recording Ld data in ROB `endif @@ -2021,8 +2027,10 @@ module mkSplitLSQ(SplitLSQ); // In that case, the data needs to be nanboxed before writing to // the register files as the Toooba FPR is 64-bit let bEn = ld_byteEn[t]; + let allowCap = ld_allowCap[t]; let dst = ld_dst[t]; let is32BitLd = (bEn[3] && !bEn[7]); + res.allowCap = allowCap; res.dst = ld_dst[t]; if (dst.Valid.isFpuReg && is32BitLd) res.data = fv_nanbox_MemTaggedData( @@ -2057,6 +2065,7 @@ module mkSplitLSQ(SplitLSQ); isMMIO: ld_isMMIO_deqLd[deqP], shiftedBE: ld_shiftedBE_deqLd[deqP], fault: ld_fault_deqLd[deqP], + allowCap: ld_allowCap[deqP], killed: ld_killed_deqLd[deqP] }; endmethod diff --git a/src_Core/RISCY_OOO/procs/lib/TlbTypes.bsv b/src_Core/RISCY_OOO/procs/lib/TlbTypes.bsv index b30a2a0..d764f39 100644 --- a/src_Core/RISCY_OOO/procs/lib/TlbTypes.bsv +++ b/src_Core/RISCY_OOO/procs/lib/TlbTypes.bsv @@ -33,7 +33,7 @@ typedef struct{ Bool write; Bool cap; } TlbReq deriving(Eq, Bits, FShow); -typedef Tuple2#(Addr, Maybe#(Exception)) TlbResp; +typedef Tuple3#(Addr, Maybe#(Exception), Bool) TlbResp; // non-blocking DTLB typedef `DTLB_REQ_NUM DTlbReqNum; @@ -180,6 +180,7 @@ typedef enum { typedef struct { Bool allowed; Exception excCode; // Only defined if !allowed + Bool allowCap; // Whether we can load caps } TlbPermissionCheck deriving(Bits, Eq, FShow); function TlbPermissionCheck hasVMPermission( @@ -244,8 +245,9 @@ function TlbPermissionCheck hasVMPermission( endcase TlbPermissionCheck ret = TlbPermissionCheck { - allowed: !fault, - excCode: access == DataStore ? StorePageFault : LoadPageFault}; + allowed: !fault, + excCode: access == DataStore ? StorePageFault : LoadPageFault, + allowCap: pte_upper_type.cap_readable}; if (!fault) begin if (cap && access == DataStore && !pte_upper_type.cap_writable) begin From a6b40e946be0c176a87436d5b7543942ce66297f Mon Sep 17 00:00:00 2001 From: Peter Rugg Date: Thu, 23 Jul 2020 11:18:07 +0100 Subject: [PATCH 6/9] Prevent using CCSeal to 'seal over' other types --- src_Core/RISCY_OOO/procs/lib/Exec.bsv | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src_Core/RISCY_OOO/procs/lib/Exec.bsv b/src_Core/RISCY_OOO/procs/lib/Exec.bsv index 779829a..2dce32b 100755 --- a/src_Core/RISCY_OOO/procs/lib/Exec.bsv +++ b/src_Core/RISCY_OOO/procs/lib/Exec.bsv @@ -258,7 +258,7 @@ function Tuple2#(CapPipe,Bool) capModify(CapPipe a, CapPipe b, CapModifyFunc fun tagged SealEntry : t(setKind(a, SENTRY)); tagged Seal : - t((validAsType(b, getAddr(b)) && isValidCap(b)) ? + t((validAsType(b, getAddr(b)) && isValidCap(b) && getKind(a) == UNSEALED) ? setKind(a, SEALED_WITH_TYPE (truncate(getAddr(b)))) : a); tagged Unseal .src : From e8aa873c2eab09e1e3ef7068bc6bc47d2d5ef0b2 Mon Sep 17 00:00:00 2001 From: Peter Rugg Date: Thu, 23 Jul 2020 11:18:31 +0100 Subject: [PATCH 7/9] Prevent 'insufficient type info' warning --- src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv b/src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv index 89dad0e..f2c4f9e 100755 --- a/src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv +++ b/src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv @@ -1251,7 +1251,7 @@ module mkSupReorderBuffer#( InstTag x, CapMem vaddr, Data store_data, ByteEn store_data_BE, Bool access_at_commit, Bool non_mmio_st_done `ifdef RVFI - , tb + , ExtraTraceBundle tb `endif ) if( all(id, readVReg(setExeMem_SB_enq)) // ordering: < enq From 97d89086a62797eb06e09336fcc26a2f671debad Mon Sep 17 00:00:00 2001 From: Peter Rugg Date: Thu, 23 Jul 2020 11:20:30 +0100 Subject: [PATCH 8/9] Bump cheri-cap-lib --- libs/cheri-cap-lib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/cheri-cap-lib b/libs/cheri-cap-lib index abfcb20..a812eda 160000 --- a/libs/cheri-cap-lib +++ b/libs/cheri-cap-lib @@ -1 +1 @@ -Subproject commit abfcb20d038c2bb4debebc562bb72453994b7917 +Subproject commit a812edaffaecc9b537f8974a528b915dda829bb6 From 27082ee2a93f43d3e21621fa5b5c7532935cd6e9 Mon Sep 17 00:00:00 2001 From: Peter Rugg Date: Thu, 23 Jul 2020 15:40:28 +0100 Subject: [PATCH 9/9] Report writes to PCC as illegal instruction, not ASR violation --- src_Core/RISCY_OOO/procs/lib/CapChecks.bsvi | 1 - src_Core/RISCY_OOO/procs/lib/Decode.bsv | 1 - src_Core/RISCY_OOO/procs/lib/Exec.bsv | 9 +++++---- 3 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src_Core/RISCY_OOO/procs/lib/CapChecks.bsvi b/src_Core/RISCY_OOO/procs/lib/CapChecks.bsvi index 3e8d8ad..722ce39 100644 --- a/src_Core/RISCY_OOO/procs/lib/CapChecks.bsvi +++ b/src_Core/RISCY_OOO/procs/lib/CapChecks.bsvi @@ -19,7 +19,6 @@ `CAP_CHECK_FIELD(src1_type_not_reserved,"src1_type_not_reserved") `CAP_CHECK_FIELD(src1_perm_subset_src2,"src1_perm_subset_src2") `CAP_CHECK_FIELD(src1_derivable,"src1_derivable") -`CAP_CHECK_FIELD(scr_read_only,"scr_read_only") `CAP_CHECK_FIELD(cfromptr_bypass,"cfromptr_bypass") `CAP_CHECK_FIELD(ccseal_bypass,"ccseal_bypass") `CAP_CHECK_FIELD(cap_exact,"cap_exact") diff --git a/src_Core/RISCY_OOO/procs/lib/Decode.bsv b/src_Core/RISCY_OOO/procs/lib/Decode.bsv index 81fbf94..537e31c 100755 --- a/src_Core/RISCY_OOO/procs/lib/Decode.bsv +++ b/src_Core/RISCY_OOO/procs/lib/Decode.bsv @@ -969,7 +969,6 @@ function DecodeResult decode(Instruction inst, Bool cap_mode); dInst.execFunc = tagged Alu Add; regs.src1 = Invalid; dInst.csr = tagged Invalid; - dInst.capChecks.scr_read_only = True; end else begin dInst.scr = Valid (scr); end diff --git a/src_Core/RISCY_OOO/procs/lib/Exec.bsv b/src_Core/RISCY_OOO/procs/lib/Exec.bsv index 2dce32b..3557a20 100755 --- a/src_Core/RISCY_OOO/procs/lib/Exec.bsv +++ b/src_Core/RISCY_OOO/procs/lib/Exec.bsv @@ -92,8 +92,6 @@ function Maybe#(CSR_XCapCause) capChecksExec(CapPipe a, CapPipe b, CapPipe ddc, result = e2(SoftwarePermViolation); else if (toCheck.src1_derivable && !isDerivable(a)) result = e1(LengthViolation); - else if (toCheck.scr_read_only && (toCheck.rn1 != 0)) - result = Valid(CSR_XCapCause{cheri_exc_reg: {1,pack(SCR_PCC)}, cheri_exc_code: PermitASRViolation}); else if (toCheck.cap_exact && !cap_exact) result = e1(RepresentViolation); return result; @@ -534,9 +532,12 @@ function Maybe#(Trap) checkForException( else if(dInst.scr matches tagged Valid .scr) begin Bool scr_has_priv = (prv >= pack(scr)[4:3]); Bool unimplemented = (scr == SCR_None); + Bool writes_scr = regs.src1 == Valid (tagged Gpr 0) ? False : True; + Bool read_only = (scr == SCR_PCC); + Bool write_deny = (writes_scr && read_only); Bool asr_deny = !getHardPerms(pcc).accessSysRegs && !( - scr == SCR_DDC); - if(!scr_has_priv || unimplemented) begin // Writes to PCC checked in capChecks + scr == SCR_DDC || scr == SCR_PCC); + if(!scr_has_priv || unimplemented || write_deny) begin exception = Valid (Exception (IllegalInst)); end else if (asr_deny) begin exception = Valid (CapException (CSR_XCapCause {cheri_exc_reg: {1'b1, pack(SCR_PCC)}, cheri_exc_code: PermitASRViolation}));